diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-21 14:39:00 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-21 14:39:00 +0200 |
| commit | 0a38e7727f3c38742704907e0c4dc60da6b99743 (patch) | |
| tree | c77e9cc64adb350459f71d8937d0895555b93772 /driver/Configuration.ml | |
| parent | f22c32dcda0e8b546e85e8ad95d0ad655e365d38 (diff) | |
| download | compcert-kvx-0a38e7727f3c38742704907e0c4dc60da6b99743.tar.gz compcert-kvx-0a38e7727f3c38742704907e0c4dc60da6b99743.zip | |
Added support for quoting for diab backend.
The diab data compiler has different quoting conventions compared
to the gnu tools.
Bug 18308.
Diffstat (limited to 'driver/Configuration.ml')
| -rw-r--r-- | driver/Configuration.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index be581e14..0a2b3eec 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -174,10 +174,12 @@ let struct_return_style = type response_file_style = | Gnu (* responsefiles in gnu compatible syntax *) + | Diab (* responsefiles in diab compatible syntax *) | Unsupported (* responsefiles are not supported *) let response_file_style = match get_config_string "response_file_style" with | "unsupported" -> Unsupported | "gnu" -> Gnu + | "diab" -> Diab | v -> bad_config "response_file_style" [v] |