aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-02-16 14:38:45 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-02-16 14:38:45 +0100
commit86cc275b2b0b6e89d2b9e5b476e6a10163a8ed42 (patch)
tree744fd7903787d85075a599fba32f6a38fbf8284b /driver
parent773058e7e21fa76097000bec6f1b9ff7e51d3b84 (diff)
downloadcompcert-86cc275b2b0b6e89d2b9e5b476e6a10163a8ed42.tar.gz
compcert-86cc275b2b0b6e89d2b9e5b476e6a10163a8ed42.zip
Added new option for static linking.
The new option -static passes the -static flag to the linker. Bug 18066.
Diffstat (limited to 'driver')
-rw-r--r--driver/Driver.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cc0d018e..4b695d57 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -497,6 +497,7 @@ Assembling options:
Linking options:
-l<lib> Link library <lib>
-L<dir> Add <dir> to search path for libraries
+ -static Prevent linking with the shared libraries
-T <file> Use <file> as linker command file
-Wl,<opt> Pass option <opt> to the linker
Tracing options:
@@ -617,6 +618,7 @@ let cmdline_actions =
(* Linking options *)
Prefix "-l", Self push_linker_arg;
Prefix "-L", Self push_linker_arg;
+ Exact "-static", Self push_linker_arg;
Exact "-T", String (fun s -> if Configuration.system = "diab" then
push_linker_arg ("-Wm"^s)
else begin