add sed script for 1.3.0 (!128) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Ralf Jung requested to merge ralf/sed into master 5 years ago

All threads resolved!

Original sed script by @tchajed. I added s/\bdom_map_filter\b/dom_map_filter_subseteq/g and s/\bseqZ_fmap\b/fmap_add_seqZ/g.

Approval is optional

Activity

Ralf Jung @jung started a thread on an old version of the diff 5 years ago

Resolved 5 years ago by Ralf Jung
Last reply by Robbert Krebbers 5 years ago

Tej Chajed @tchajed started a thread on an outdated change in commit 88e60b76 5 years ago

Resolved 5 years ago by Ralf Jung

Ralf Jung added 1 commit 5 years ago

added 1 commit

1eaa5cf6 - add sed script for 1.3.0

Compare with previous version

Ralf Jung @jung 5 years ago

Author Owner

@robbertkrebbers any feedback for this?

Ralf Jung added 1 commit 5 years ago

added 1 commit

809acb6d - adjust to GNU sed

Compare with previous version

Robbert Krebbers @robbertkrebbers 5 years ago

Owner

Thanks for updating, @jung! Merging.

Robbert Krebbers mentioned in commit 5 years ago

mentioned in commit 5439c7d5

Robbert Krebbers merged 5 years ago

merged

Ralf Jung resolved all threads 5 years ago

resolved all threads

Please register or sign in to reply