# HG changeset patch
# User wenzelm
# Date 1030439274 -7200
# Node ID 70de987e9fe3ce4c42c8c7044f282f575c3677b8
# Parent  131bb248504dc1e6676028e1a6ad4bcf8dd956ed
check_file: disallow current dir (typically "");

diff -r 131bb248504d -r 70de987e9fe3 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Aug 27 11:07:01 2002 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Aug 27 11:07:54 2002 +0200
@@ -80,7 +80,12 @@
 
     fun find_dir dir =
       get_first (find_ext (Path.append dir path)) ml_exts;
-  in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
+
+    val paths =
+      if Path.is_current path then error "Bad file specification"
+      else if Path.is_basic path then ! load_path
+      else [Path.current];
+  in get_first find_dir paths end;
 
 
 (* load_file *)