diff options
Diffstat (limited to 'write_makefile.sh')
| -rwxr-xr-x | write_makefile.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/write_makefile.sh b/write_makefile.sh index 6aca660..d5c0fa9 100755 --- a/write_makefile.sh +++ b/write_makefile.sh @@ -14,10 +14,10 @@ # CC0 1.0 Universal License for more details. if [ ! -e record.conf ]; then - echo Record of configuration "'record.conf'" does not exist. >&2 + echo "Record of configuration 'record.conf' does not exist." >&2 exit 1 elif [ "$(head -n 1 record.conf | cut -c -9)x" != "srcdir = x" ]; then - echo Record of configuration "'record.conf'" is invalid. >&2 + echo "Record of configuration 'record.conf' is invalid." >&2 exit 2 fi |