summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Sergey Mironov <grrwlf@gmail.com>2013-11-06 13:54:07 +0400
committerGravatar Sergey Mironov <grrwlf@gmail.com>2013-11-06 13:54:07 +0400
commitc4b4749083acf290d28b53a0194c35ce247c3c15 (patch)
treec97ea033de428e67db07a102d4c7c3bc7cb4ac8c
parent50cfe0f997e94afdfa78b953125f8e9e498069bf (diff)
Add -print-cinlude command line option
-rw-r--r--src/main.mlton.sml4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index d176efcc..e68ecdd8 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -58,6 +58,8 @@ fun oneRun args =
raise Code OS.Process.success)
fun printCCompiler () = (print ((Settings.getCCompiler ()) ^ "\n");
raise Code OS.Process.success)
+ fun printCInclude () = (print ((Config.includ) ^ "\n");
+ raise Code OS.Process.success)
fun doArgs args =
case args of
@@ -71,6 +73,8 @@ fun oneRun args =
doArgs rest)
| "-print-ccompiler" :: rest =>
printCCompiler ()
+ | "-print-cinclude" :: rest =>
+ printCInclude ()
| "-ccompiler" :: ccomp :: rest =>
(Settings.setCCompiler ccomp;
doArgs rest)