# HG changeset patch
# User wenzelm
# Date 1313155812 -7200
# Node ID c1da9897b6c982f7761300dc31505f87f4993f39
# Parent  8848867501fb8af7783fffdad0c462bc0898652b
allow "$" within basic path elements (NB: initial "$" refers to path variable);

diff -r 8848867501fb -r c1da9897b6c9 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Aug 12 15:28:30 2011 +0200
+++ b/src/Pure/General/path.ML	Fri Aug 12 15:30:12 2011 +0200
@@ -51,7 +51,7 @@
   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
   | check_elem chs =
-      (case inter (op =) ["/", "\\", "$", ":"] chs of
+      (case inter (op =) ["/", "\\", ":"] chs of
         [] => chs
       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);