From eb2844b87fa0e176bd65466d7ab7d16666344406 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 10 Aug 2016 13:31:25 +0200
Subject: Added missing begin end around quoting. Bug 18308.

---
 driver/Driveraux.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'driver/Driveraux.ml')

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
 
-- 
cgit