Skip to content
Snippets Groups Projects
Commit d8ad1852 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Properly escape ' in sed script.

parent e50a5b09
No related branches found
No related tags found
1 merge request!307Clean up `empty{',_inv,_iff}` lemmas.
Pipeline #51280 passed
...@@ -146,7 +146,7 @@ The following `sed` script should perform most of the renaming ...@@ -146,7 +146,7 @@ The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice. Note that the script is not idempotent, do not run it twice.
``` ```
sed -i -E ' sed -i -E -f- $(find theories -name "*.v") <<EOF
s/\bdecide_left\b/decide_True_pi/g s/\bdecide_left\b/decide_True_pi/g
s/\bdecide_right\b/decide_False_pi/g s/\bdecide_right\b/decide_False_pi/g
# Permutation # Permutation
...@@ -195,7 +195,7 @@ s/\bsize_empty_inv\b/size_empty_iff/g ...@@ -195,7 +195,7 @@ s/\bsize_empty_inv\b/size_empty_iff/g
s/\bdom_empty_inv(_L|)\b/dom_empty_iff\1/g s/\bdom_empty_inv(_L|)\b/dom_empty_iff\1/g
s/\bgmultiset_elements_empty('|_inv)\b/gmultiset_elements_empty_iff/g s/\bgmultiset_elements_empty('|_inv)\b/gmultiset_elements_empty_iff/g
s/\bgmultiset_size_empty_inv\b/gmultiset_size_empty_iff/g s/\bgmultiset_size_empty_inv\b/gmultiset_size_empty_iff/g
' $(find theories -name "*.v") EOF
``` ```
## std++ 1.5.0 (2021-02-16) ## std++ 1.5.0 (2021-02-16)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment