# HG changeset patch
# User wenzelm
# Date 1189967143 -7200
# Node ID 98689b0e595684e9a0514d29803700c2d63a363b
# Parent  d5c5d2e13fbf0f13393e85f7c064ee51363ce826
use_file: added ``tune'' argument;

diff -r d5c5d2e13fbf -r 98689b0e5956 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Sun Sep 16 15:36:57 2007 +0200
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sun Sep 16 20:25:43 2007 +0200
@@ -34,8 +34,8 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file output verbose name =
+fun use_file tune output verbose name =
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_text name output verbose txt end;
+  in use_text tune name output verbose txt end;