summaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-07-08 08:36:06 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-07-08 08:36:06 +0000
commit56257af93c1b0785d44e3feba9574e77250d420c (patch)
tree3ade697e04dae62d4f999bf79f29f91576dfee75 /configure
parentbd1a4956257638793d3a6a3ffcee1773541d601b (diff)
Add option -no-runtime-lib.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2293 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure5
1 files changed, 4 insertions, 1 deletions
diff --git a/configure b/configure
index 0245e93..65bfbbe 100755
--- a/configure
+++ b/configure
@@ -17,6 +17,7 @@ bindir='$(PREFIX)/bin'
libdir='$(PREFIX)/lib/compcert'
toolprefix=''
target=''
+has_runtime_lib=true
usage='Usage: ./configure [options] target
@@ -37,6 +38,7 @@ Options:
-bindir <dir> Install binaries in <dir>
-libdir <dir> Install libraries in <dir>
-toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref>
+ -no-runtime-lib Do not compile nor install the runtime support library
'
# Parse command-line arguments
@@ -52,6 +54,8 @@ while : ; do
libdir="$2"; shift;;
-toolprefix|--toolprefix)
toolprefix="$2"; shift;;
+ -no-runtime-lib)
+ has_runtime_lib=false; shift;;
*)
if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
target="$1";;
@@ -62,7 +66,6 @@ done
# Per-target configuration
cchecklink=false
-has_runtime_lib=true
casmruntime=""
asm_supports_cfi=""