# 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;