author | wenzelm |
Sat, 27 Nov 2010 15:58:36 +0100 | |
changeset 40746 | f57ca096d8c9 |
parent 40745 | 1dabcda202c3 |
child 40747 | 889b7545a408 |
--- a/src/Pure/General/file.ML Sat Nov 27 15:45:20 2010 +0100 +++ b/src/Pure/General/file.ML Sat Nov 27 15:58:36 2010 +0100 @@ -37,7 +37,11 @@ val platform_path = Path.implode o Path.expand; -val shell_quote = enclose "'" "'"; +fun shell_quote s = + if exists_string (fn c => c = "'") s then + error ("Illegal single quote in path specification: " ^ quote s) + else enclose "'" "'" s; + val shell_path = shell_quote o platform_path;