isabelle: src/Tools/install_html.sh@889d99613720 (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
1406 dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	9	rsh www4 "rm -r .html-data/isabelle/*; mkdir .html-data/isabelle/Tools; \
1469 fb9ccf06dfe8 fixed two little bugs clasohm parents: 1406 diff changeset	10	chmod og-w .html-data/isabelle/Tools"
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	11	endif
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	12
1406 dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	13	rcp index.html www4:.html-data/isabelle
2804 889d99613720 fixed Tools path; wenzelm parents: 2221 diff changeset	14	rcp ../Tools/*.gif www4:.html-data/isabelle/Tools
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	15
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	16	if ( "$*" == "" ) then
2221 39077a563a82 Replaced LK&Modal by Sequents nipkow parents: 2179 diff changeset	17	rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF Sequents ZF \
1406 dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	18	www4:.html-data/isabelle
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	19	else
1406 dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	20	rcp -r $* www4:.html-data/isabelle
1315 1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	21	endif
1469 fb9ccf06dfe8 fixed two little bugs clasohm parents: 1406 diff changeset	22	rsh www4 "chgrp -R isabelle .html-data/isabelle/; chmod -R g+w .html-data/isabelle/"

author	wenzelm
	Tue, 18 Mar 1997 14:35:10 +0100
changeset 2804	889d99613720
parent 2221	39077a563a82
child 2824	ec170ea5243e
permissions	-rwxr-xr-x