aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
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