author | wenzelm |
Mon, 23 Jul 2012 15:44:42 +0200 | |
changeset 48446 | 8f611bc3650b |
parent 48445 | cb4136e4cabf |
child 48447 | ef600ce4559c |
--- a/src/Pure/General/file.ML Mon Jul 23 15:05:05 2012 +0200 +++ b/src/Pure/General/file.ML Mon Jul 23 15:44:42 2012 +0200 @@ -45,11 +45,7 @@ val platform_path = Path.implode o Path.expand; -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_quote = enclose "'" "'"; val shell_path = shell_quote o platform_path;