# HG changeset patch
# User nipkow
# Date 847801236 -3600
# Node ID 018906568ef0e530eed3dbd89e8472d54ca66f7f
# Parent  acb0afbf61a306b243eb5c1a53711cdf25b34769
Now moves all Tool/*gif files.

diff -r acb0afbf61a3 -r 018906568ef0 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 \