From fd5a2ff53dee8b48c572e85819a8d3bd8ac916ec Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 6 Apr 2020 12:16:00 +0200 Subject: [PATCH] add missing sed flag --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b1d7e70a..bc20a165 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -63,7 +63,7 @@ Noteworthy additions and changes: 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 ' +sed -i ' s/\bdom_map_filter\b/dom_map_filter_subseteq/g s/\bfmap_seq\b/fmap_S_seq/g s/\bseqZ_fmap\b/fmap_add_seqZ/g -- GitLab