# HG changeset patch
# User berghofe
# Date 960372926 -7200
# Node ID 17c5edf1706b23358b3448378eff9981f70486a1
# Parent  a5bfcd4c2a5e022baa559dcaf74cfb9706a65dfc
Exported system_command.

diff -r a5bfcd4c2a5e -r 17c5edf1706b 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