diff options
| -rwxr-xr-x | update-from-external.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/update-from-external.sh b/update-from-external.sh index 397dac87..18ada952 100755 --- a/update-from-external.sh +++ b/update-from-external.sh @@ -7,7 +7,7 @@ # # Does not create a GIT commit. -if [ $# -eq 0 ]; then +if [ $# -ne 1 ]; then echo "usage: $0 <version>" echo " where <version> is the version number, e.g. 7.7.3" exit 1 |