aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Commandline.ml
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2016-08-17 16:32:56 +0200
committerMichael Schmidt <github@mschmidt.me>2016-08-17 16:32:56 +0200
commite0f0f573a4a8fc1f564a31388afa9c23e48bb016 (patch)
treeb7c004b3aae01c79bef8c8914e759a1e3ce358f7 /driver/Commandline.ml
parent18fcf2ffef8b4ba5eb0624b15371e93b4ac88cfe (diff)
parente2b4459ccd1b0f8436cb70a631772d715e642dcd (diff)
downloadcompcert-e0f0f573a4a8fc1f564a31388afa9c23e48bb016.tar.gz
compcert-e0f0f573a4a8fc1f564a31388afa9c23e48bb016.zip
fix merge conflicts
Diffstat (limited to 'driver/Commandline.ml')
-rw-r--r--driver/Commandline.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index 0a2c8fca..d125736a 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -16,6 +16,7 @@
(* Parsing of command-line flags and arguments *)
open Printf
+open Responsefile
type pattern =
| Exact of string
@@ -99,4 +100,9 @@ let parse_array spec argv first last =
in parse first
let parse_cmdline spec =
- parse_array spec Sys.argv 1 (Array.length Sys.argv - 1)
+ try
+ let argv = expandargv Sys.argv in
+ parse_array spec argv 1 (Array.length argv - 1)
+ with Responsefile.Error s ->
+ eprintf "%s" s;
+ exit 2