# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1409834414 14400
# Node ID 88841212f0bae33c215ecdbd9e19dc18869ca401
# Parent  7214a14a6fe24a001fb27883cd0b7623656c4929
In computing command lines, put filenames inside of quotes, to support spaces and other funky characters nicely

diff -r 7214a14a6fe2 -r 88841212f0ba src/compiler.sml
--- a/src/compiler.sml	Sat Aug 30 08:48:41 2014 -0400
+++ b/src/compiler.sml	Thu Sep 04 08:40:14 2014 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2012, Adam Chlipala
+(* Copyright (c) 2008-2012, 2014, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -1483,7 +1483,10 @@
 
 val toSqlify = transform sqlify "sqlify" o toMono_opt2
 
-val escapeFilename = String.translate (fn #" " => "\\ " | #"\"" => "\\\"" | #"'" => "\\'" | ch => str ch)
+fun escapeFilename s =
+    "\""
+    ^ String.translate (fn #"\"" => "\\\"" | #"\\" => "\\\\" | ch => str ch) s
+    ^ "\""
 
 val beforeC = ref (fn () => ())