From 66cb2a32e2321d1d0c244623b3a9cb8274d203f3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 30 Mar 2010 12:19:52 +0000
Subject: [PATCH] Options -I -D -U with a space
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
driver/Driver.ml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d7c93641f..255b60047 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -294,6 +294,9 @@ let cmdline_actions =
let f_opt name ref =
["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
[
+ "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
+ "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
+ "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
"-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
"-[lL].", Self(fun s -> linker_options := s :: !linker_options);
"-o$", String(fun s -> exe_name := s);
--
GitLab