# HG changeset patch
# User wenzelm
# Date 1343051082 -7200
# Node ID 8f611bc3650ba86041420357088fdb9dc8467207
# Parent  cb4136e4cabfadb3e81bad696e649c74377f6eee
removed redundant check (cf. a8ed41b6280b);

diff -r cb4136e4cabf -r 8f611bc3650b src/Pure/General/file.ML
--- 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;