summaryrefslogtreecommitdiff
path: root/driver
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-14 08:05:36 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-07-14 08:05:36 +0000
commitbd85aba84475dd956af21c461c44a584958099d1 (patch)
treebab1cefe9f84210559a4716a070d79967b60f2b5 /driver
parent48b839d15e69c3c9995ca3c25e6a7c4730224292 (diff)
Support for indirect symbols under MacOS X (final).
Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r--driver/Driver.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 881a895..3ee4b6b 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -60,7 +60,7 @@ let preprocess ifile ofile =
let cmd =
sprintf "%s -D__COMPCERT__ %s %s %s %s"
Configuration.prepro
- (if Configuration.need_stdlib_wrapper
+ (if Configuration.has_runtime_lib
then sprintf "-I%s" !stdlib_path
else "")
(quote_options !prepro_options)
@@ -210,7 +210,7 @@ let linker exe_name files =
Configuration.linker
(Filename.quote exe_name)
(quote_options files)
- (if Configuration.need_stdlib_wrapper
+ (if Configuration.has_runtime_lib
then sprintf "-L%s -lcompcert" !stdlib_path
else "") in
if command cmd <> 0 then exit 2