changeset 2067:88841212f0ba

In computing command lines, put filenames inside of quotes, to support spaces and other funky characters nicely
author Adam Chlipala <adam@chlipala.net>
date Thu, 04 Sep 2014 08:40:14 -0400
parents 7214a14a6fe2
children b6adfe99bb08
files src/compiler.sml
diffstat 1 files changed, 5 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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 () => ())