# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1220647693 14400
# Node ID c8070689f5ca1d0cbcc5f829be166db3438bdbb6
# Parent  91e247c68ee8b9e56d331f554c7ecab39bc81822
Switch [input_line] to [read_line]

diff -r 91e247c68ee8 -r c8070689f5ca tools/make_template.ml
--- a/tools/make_template.ml	Fri Sep 05 16:46:32 2008 -0400
+++ b/tools/make_template.ml	Fri Sep 05 16:48:13 2008 -0400
@@ -1,10 +1,10 @@
-let input_line () = 
+let read_line () = 
   try
-    Some (input_line stdin)
+    Some (read_line ())
   with End_of_file -> None
 
 let rec initial last_was_empty =
-  match input_line () with
+  match read_line () with
   | None -> ()
   | Some "(* begin thide *)" ->	thide last_was_empty
   | Some "" ->
@@ -23,7 +23,7 @@
       end
 
 and comment last_was_empty =
-  match input_line () with
+  match read_line () with
   | None -> ()
   | Some line ->
       if String.length line >= 2 && line.[String.length line - 2] = '*'
@@ -33,7 +33,7 @@
 	comment last_was_empty
 
 and thide last_was_empty =
-  match input_line () with
+  match read_line () with
   | None -> ()
   | Some "(* end thide *)" -> initial last_was_empty
   | Some _ -> thide last_was_empty