Nils Winkler f29a195f49 Make sed replacements work for both BSD and GNU sed ... Fixes #1411		2019-07-31 08:50:33 +02:00
..
available	Make sed replacements work for both BSD and GNU sed	2019-07-31 08:50:33 +02:00