isabelle: src/Tools/install_html.sh@b8a8ae2e5de1 (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
dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	14	rcp Tools/*_arrow.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
1b731d0b5ad3 added optional parameters clasohm parents: 1312 diff changeset	17	rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal 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	oheimb
	Wed, 03 Apr 1996 19:27:14 +0200
changeset 1637	b8a8ae2e5de1
parent 1469	fb9ccf06dfe8
child 2179	018906568ef0
permissions	-rwxr-xr-x