Exported system_command.
authorberghofe
Wed, 07 Jun 2000 12:15:26 +0200
changeset 9046 17c5edf1706b
parent 9045 a5bfcd4c2a5e
child 9047 810966809663
Exported system_command.
src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Jun 07 12:14:57 2000 +0200
+++ b/src/Pure/General/file.ML	Wed Jun 07 12:15:26 2000 +0200
@@ -19,6 +19,7 @@
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
+  val system_command: string -> unit
   val copy: Path.T -> Path.T -> unit
   eqtype info
   val info: Path.T -> info option