src/Tools/install_html.sh

--- a/src/Tools/install_html.sh	Tue Nov 12 11:57:10 1996 +0100
+++ b/src/Tools/install_html.sh	Tue Nov 12 13:20:36 1996 +0100
@@ -11,7 +11,7 @@
 endif
 
 rcp index.html www4:.html-data/isabelle
-rcp Tools/*_arrow.gif www4:.html-data/isabelle/Tools
+rcp Tools/*.gif www4:.html-data/isabelle/Tools
 
 if ( "$*" == "" ) then
   rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal ZF \