diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-28 10:40:53 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-28 10:40:53 +0100 |
commit | 14f3f0dfb90c74b7e1bc96c4aee74fb88dd7923b (patch) | |
tree | c44d0a8bb2a24ecf077a1817f0145b32045ca6c0 | |
parent | c58e3bdadde3ab60c982bdd036964987add72bee (diff) | |
download | compcert-14f3f0dfb90c74b7e1bc96c4aee74fb88dd7923b.tar.gz compcert-14f3f0dfb90c74b7e1bc96c4aee74fb88dd7923b.zip |
Only for options with value.
-rwxr-xr-x | configure | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -64,9 +64,9 @@ while : ; do -toolprefix|--toolprefix) toolprefix="$2"; shift;; -no-runtime-lib) - has_runtime_lib=false; shift;; + has_runtime_lib=false;; -no-checklink) - build_checklink=false; shift;; + build_checklink=false;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; |