summaryrefslogtreecommitdiff
path: root/src
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
commit4800d8054ee97979a4706daa178127985957b016 (patch)
treec97ea033de428e67db07a102d4c7c3bc7cb4ac8c /src
parent64169805c117326ccd9af8198cd16d581cc25c2d (diff)
Add -print-cinlude command line option
Diffstat (limited to 'src')
-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)