changeset 1602 | 699ad6611c1e |
parent 1598 | 6f4d995590fd |
child 1603 | 44bc1417b07c |
--- a/src/Pure/Thy/thy_read.ML Thu Mar 21 13:02:26 1996 +0100 +++ b/src/Pure/Thy/thy_read.ML Fri Mar 22 12:06:08 1996 +0100 @@ -671,9 +671,9 @@ val fname = tack_on path ("." ^ t ^ "_sub.html"); val out = if file_exists fname then - open_append fname handle Io s => - (warning ("Unable to write to file ." ^ - fname); raise Io s) + open_append fname handle e => + (warning ("Unable to write to file " ^ + fname); raise e) else raise MK_HTML; in output (out, " |\n \\__<A HREF=\"" ^