diff options
| author |  Stefan Fuchs <sfuchs@gmx.de> | 2017-11-04 18:05:35 +0100 |
|---|---|---|
| committer |  Dirk Hohndel <dirk@hohndel.org> | 2017-11-04 10:55:11 -0700 |
| commit | 76286c4ece36baff3aaabb8a4e1252997d8ad7c4 (patch) | |
| tree | 675ce611c593b68d9d7ddf8d03c5b01efb3f984a /scripts | |
| parent | 617c6d3564e562df580824280654d9edaf238084 (diff) | |
| download | subsurface-76286c4ece36baff3aaabb8a4e1252997d8ad7c4.tar.gz | |
Rename README to README.md in some scripts, makefiles,...
Was needed after the file itself was renamed.
Signed-off-by: Stefan Fuchs <sfuchs@gmx.de>
Diffstat (limited to 'scripts')
| -rwxr-xr-x | scripts/check-version | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/check-version b/scripts/check-version index 1770ba5f4..525d65d22 100755 --- a/scripts/check-version +++ b/scripts/check-version @@ -15,7 +15,7 @@ set -eu #set -x # You would typically add/remove files to/from the list -files="Documentation/user-manual.txt Makefile README ReleaseNotes/ReleaseNotes.txt" +files="Documentation/user-manual.txt Makefile README.md ReleaseNotes/ReleaseNotes.txt" whine() { echo "$0: $*" >&2 |