# HG changeset patch
# User wenzelm
# Date 920977762 -3600
# Node ID 4a423e8a0b5404c5c5b26f66dffb4cf4eac6af4e
# Parent  128e592f54896874b747f5a3360c48441593e9d4
added mkdir;

diff -r 128e592f5489 -r 4a423e8a0b54 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Mar 09 12:09:05 1999 +0100
+++ b/src/Pure/General/file.ML	Tue Mar 09 12:09:22 1999 +0100
@@ -22,6 +22,7 @@
   eqtype info
   val info: Path.T -> info option
   val exists: Path.T -> bool
+  val mkdir: Path.T -> unit
 end;
 
 structure File: FILE =
@@ -87,4 +88,9 @@
 val exists = is_some o info;
 
 
+(* mkdir *)
+
+fun mkdir path = (execute ("mkdir -p " ^ enclose "'" "'" (sysify path)); ());
+
+
 end;