author | wenzelm |
Fri, 18 Jul 1997 13:35:36 +0200 | |
changeset 3527 | b894f4c13df5 |
parent 3526 | df4d0dad2b4e |
child 3528 | f4b28e25ba99 |
--- a/src/Pure/Thy/thy_read.ML Fri Jul 18 13:35:15 1997 +0200 +++ b/src/Pure/Thy/thy_read.ML Fri Jul 18 13:35:36 1997 +0200 @@ -717,7 +717,7 @@ val theory_list = TextIO.openAppend (tack_on (!index_path) ".theory_list.txt") handle _ => (make_html := false; - writeln ("Warning: Cannot write to " ^ + warning ("Cannot write to " ^ (!index_path) ^ " while making HTML files.\n\ \HTML generation has been switched off.\n\ \Call init_html() from within a \