aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavierleroy@users.noreply.github.com>2015-12-19 16:43:40 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2015-12-19 16:43:40 +0100
commitcf6be884d6ac2713553ec18339314211716d8af4 (patch)
tree0201fcc8e0df369f23a2397a1de38f69c8cd3ad7 /driver/Driver.ml
parent0c9eaaf7d6cb229437bac8d3b11c88e2b05268a8 (diff)
parent36fa22560e2a289c9f75f0fe058b72eaad6d53b4 (diff)
downloadcompcert-cf6be884d6ac2713553ec18339314211716d8af4.tar.gz
compcert-cf6be884d6ac2713553ec18339314211716d8af4.zip
Merge pull request #79 from AbsInt/config-option
Add "-conf <filename>" command-line option. Support relative paths for stdlib and tools.
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 9b0e8f13..db3031b4 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -570,7 +570,8 @@ let cmdline_actions =
Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n);
Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n);
(* Target processor options *)
- Exact "--conf", String (fun _ -> ()); (* Ignore option since it is already handled *)
+ Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *)
+ Exact "-target", String (fun _ -> ()); (* Ignore option since it is already handled *)
Exact "-mthumb", Set option_mthumb;
Exact "-marm", Unset option_mthumb;
(* Assembling options *)