diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-21 14:45:44 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-21 14:45:44 +0200 |
commit | 951c37603e2a807b116f91d7390bd6e641d8092b (patch) | |
tree | 7d2d8863986b525842aaa5dacf7456f098f615c6 | |
parent | 0a38e7727f3c38742704907e0c4dc60da6b99743 (diff) | |
download | compcert-951c37603e2a807b116f91d7390bd6e641d8092b.tar.gz compcert-951c37603e2a807b116f91d7390bd6e641d8092b.zip |
Corrected diab quoting. Bug 18308
-rw-r--r-- | driver/Driveraux.ml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 1ee39e8e..a773b37c 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -69,17 +69,20 @@ let gnu_quote arg = Buffer.add_char buf c) arg; Buffer.contents buf -let re_whitespace = Str.regexp ".*[ \t\n\r]" +let re_quote = Str.regexp ".*[ \t\n\r\"]" let diab_quote arg = let buf = Buffer.create ((String.length arg) + 8) in - let doublequote = Str.string_match re_whitespace arg 0 in - if doublequote then Buffer.add_char buf '"'; - String.iter (fun c -> - if c = '"' then Buffer.add_char buf '\\'; - Buffer.add_char buf c) arg; - if doublequote then Buffer.add_char buf '"'; - Buffer.contents buf + let doublequote = Str.string_match re_quote arg 0 in + if doublequote then begin + Buffer.add_char buf '"'; + String.iter (fun c -> + if c = '"' then Buffer.add_char buf '\\'; + Buffer.add_char buf c) arg; + if doublequote then Buffer.add_char buf '"'; + Buffer.contents buf + end else + arg let command ?stdout args = let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in |