diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-30 09:51:24 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-03-30 09:51:24 +0200 |
commit | 09bfabebc2e06bf3486b14ae088876890ec8a8d7 (patch) | |
tree | 7cf757fd62384edff4a9eb2129169f6d6df0be05 | |
parent | 732bc15341b2e43e5ea21073f3066dcd30660f03 (diff) | |
parent | 14f3f0dfb90c74b7e1bc96c4aee74fb88dd7923b (diff) | |
download | compcert-09bfabebc2e06bf3486b14ae088876890ec8a8d7.tar.gz compcert-09bfabebc2e06bf3486b14ae088876890ec8a8d7.zip |
Merge branch 'master' into dwarf
-rwxr-xr-x | configure | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -65,9 +65,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";; |