From 420e57f67edb94250ddbf64d8ba35046479d4d4d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Thu, 29 Oct 2020 11:00:00 +0100 Subject: [PATCH] Update sed script. --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fa7cf357..d4f13b19 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -43,7 +43,8 @@ The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): ``` sed -i ' -s/\bQp_not_plus_q_ge_1\b/Qp_not_plus_ge/g +s/\bQp_plus/Qp_add/g +s/\bQp_mult/Qp_mul/g ' $(find theories -name "*.v") ``` -- GitLab