# HG changeset patch
# User wenzelm
# Date 1290869916 -3600
# Node ID f57ca096d8c935a449e06a0c1ffede8a24c52a5e
# Parent  1dabcda202c35278a45729afa10da252846677e3
explicit check for requirement;

diff -r 1dabcda202c3 -r f57ca096d8c9 src/Pure/General/file.ML
--- 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;