diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-10 13:31:25 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-08-10 13:31:25 +0200 |
| commit | eb2844b87fa0e176bd65466d7ab7d16666344406 (patch) | |
| tree | f4d812309d7bde69c1e94cfce759e0e99f943c8c /driver/Driveraux.ml | |
| parent | 951c37603e2a807b116f91d7390bd6e641d8092b (diff) | |
| download | compcert-kvx-eb2844b87fa0e176bd65466d7ab7d16666344406.tar.gz compcert-kvx-eb2844b87fa0e176bd65466d7ab7d16666344406.zip | |
Added missing begin end around quoting. Bug 18308.
Diffstat (limited to 'driver/Driveraux.ml')
| -rw-r--r-- | driver/Driveraux.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index a773b37c..de1326ce 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -62,10 +62,10 @@ let command stdout args = let gnu_quote arg = let len = String.length arg in let buf = Buffer.create len in - String.iter (fun c -> match c with + String.iter (fun c -> begin match c with | ' ' | '\t' | '\r' | '\n' | '\\' | '\'' | '"' -> Buffer.add_char buf '\\' - | _ -> (); + | _ -> () end; Buffer.add_char buf c) arg; Buffer.contents buf |