Added function "file_exists".
authorberghofe
Wed, 06 Aug 1997 00:29:54 +0200
changeset 3606 5d7073700fbc
parent 3605 d372fb6ec393
child 3607 a4b9ed94907a
Added function "file_exists".
src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Aug 06 00:29:02 1997 +0200
+++ b/src/Pure/library.ML	Wed Aug 06 00:29:54 1997 +0200
@@ -873,6 +873,8 @@
                   (rm_points (space_explode "/" (tack_on cwd file)) [])
   end;
 
+fun file_exists file = (file_info file <> "");
+
 
 (** misc functions **)