isabelle: src/Tools/install_html.sh@cdfa3ffcead2 (annotated)

1310 3d773439d844 removed buggy FTP scripts and replaced them by a script for transfer clasohm parents: diff changeset	1	#!/bin/csh
3d773439d844 removed buggy FTP scripts and replaced them by a script for transfer clasohm parents: diff changeset	2	# Executed from the main Isabelle directory, this script transfers all
3d773439d844 removed buggy FTP scripts and replaced them by a script for transfer clasohm parents: diff changeset	3	# files needed for the HTML version of Isabelle's theories to the HTTP
3d773439d844 removed buggy FTP scripts and replaced them by a script for transfer clasohm parents: diff changeset	4	# server.
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	5	# If you don't want to copy all the logics, you can supply the names of
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	6	# the wanted ones as parameters as in "install_html.sh HOL HOLCF".
1310 3d773439d844 removed buggy FTP scripts and replaced them by a script for transfer clasohm parents: diff changeset	7
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	8	if ( "$*" == "" ) then
1349 ef26adb4e5b6 added local index.html files to rm_html.sh; clasohm parents: 1315 diff changeset	9	rsh hpbroy12 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools"
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	10	endif
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	11
1349 ef26adb4e5b6 added local index.html files to rm_html.sh; clasohm parents: 1315 diff changeset	12	rcp index.html hpbroy12:.html-data/isabelle
ef26adb4e5b6 added local index.html files to rm_html.sh; clasohm parents: 1315 diff changeset	13	rcp Tools/*_arrow.gif hpbroy12:.html-data/isabelle/Tools
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	14
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	15	if ( "$*" == "" ) then
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	16	rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal ZF \
1349 ef26adb4e5b6 added local index.html files to rm_html.sh; clasohm parents: 1315 diff changeset	17	hpbroy12:.html-data/isabelle
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	18	else
1349 ef26adb4e5b6 added local index.html files to rm_html.sh; clasohm parents: 1315 diff changeset	19	rcp -r $* hpbroy12:.html-data/isabelle
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	20	endif

author	clasohm
	Wed, 13 Dec 1995 14:14:06 +0100
changeset 1403	cdfa3ffcead2
parent 1349	ef26adb4e5b6
child 1406	dc73ca67b5ac
permissions	-rwxr-xr-x