diff options
-rwxr-xr-x | configure | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -91,6 +91,7 @@ warn=0 | |||
91 | debug=0 | 91 | debug=0 |
92 | address=0 | 92 | address=0 |
93 | memory=0 | 93 | memory=0 |
94 | unknown=0 | ||
94 | old_cc="$CC" | 95 | old_cc="$CC" |
95 | old_cflags="$CFLAGS" | 96 | old_cflags="$CFLAGS" |
96 | OBJC='$(OBJZ) $(OBJG)' | 97 | OBJC='$(OBJZ) $(OBJG)' |
@@ -144,12 +145,12 @@ case "$1" in | |||
144 | --sanitize) address=1; shift ;; | 145 | --sanitize) address=1; shift ;; |
145 | --address) address=1; shift ;; | 146 | --address) address=1; shift ;; |
146 | --memory) memory=1; shift ;; | 147 | --memory) memory=1; shift ;; |
147 | *) | 148 | *) unknown=1; echo "unknown option ignored: $1" | tee -a configure.log; shift;; |
148 | echo "unknown option: $1" | tee -a configure.log | ||
149 | echo "$0 --help for help" | tee -a configure.log | ||
150 | leave 1;; | ||
151 | esac | 149 | esac |
152 | done | 150 | done |
151 | if test $unknown -eq 1; then | ||
152 | echo "$0 --help for help" | tee -a configure.log | ||
153 | fi | ||
153 | 154 | ||
154 | # temporary file name | 155 | # temporary file name |
155 | test=ztest$$ | 156 | test=ztest$$ |