Matthias Andree 1240f9c8de Tools/scripts/sed_checked.sh: reword sed warning ...

The original wording was misleading and might have mistaken for
identical file names, but what is meant is that the sed run did not
introduce changes to the file's __content__. Reword accordingly.

2020-01-12 12:06:52 +00:00

..

scripts

Tools/scripts/sed_checked.sh: reword sed warning

2020-01-12 12:06:52 +00:00

make_index

…

make_readmes

…