removed image borders from index.html files
authorclasohm
Fri, 03 Nov 1995 12:00:46 +0100
changeset 1320 b94ef890dbf2
parent 1319 f63b036ad690
child 1321 9a6e7bd2bfaf
removed image borders from index.html files
src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Nov 02 14:17:26 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Nov 03 12:00:46 1995 +0100
@@ -1053,10 +1053,10 @@
                   "<H3>" ^ space_implode "/" subdir ^ "</H3>\n")
                 else "") ^
                "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^
-               tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^
+               tack_on gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^
                "<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^
                tack_on gif_path "blue_arrow.gif\
-               \\" ALT = /\\></A> <A HREF = \"" ^ tpath ^
+               \\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^
                ".html\">" ^ tname ^ "</A><BR>\n" ^
                main_entries ts subdir
             end;