1.1 --- a/src/Pure/General/file.ML	Sat Nov 27 15:45:20 2010 +0100
     1.2 +++ b/src/Pure/General/file.ML	Sat Nov 27 15:58:36 2010 +0100
     1.3 @@ -37,7 +37,11 @@
     1.4  
     1.5  val platform_path = Path.implode o Path.expand;
     1.6  
     1.7 -val shell_quote = enclose "'" "'";
     1.8 +fun shell_quote s =
     1.9 +  if exists_string (fn c => c = "'") s then
    1.10 +    error ("Illegal single quote in path specification: " ^ quote s)
    1.11 +  else enclose "'" "'" s;
    1.12 +
    1.13  val shell_path = shell_quote o platform_path;
    1.14  
    1.15