# HG changeset patch
# User clasohm
# Date 815396446 -3600
# Node ID b94ef890dbf2a4a14b0e184eb16ff1f5d1d0cba5
# Parent  f63b036ad690389ff70ad02159e48c2648b5883b
removed image borders from index.html files

diff -r f63b036ad690 -r b94ef890dbf2 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;