isabelle: src/Tools/install_html.sh@dc73ca67b5ac (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; \
dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	10	chmod o-w 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
1406 dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	22	rsh www4 "chgrp -R isabelle .html-data/isabelle/*; \
dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	23	chmod -R g+w .html-data/isabelle/*"
dc73ca67b5ac added chmod and chgrp clasohm parents: 1349 diff changeset	24

author	clasohm
	Fri, 15 Dec 1995 12:23:56 +0100
changeset 1406	dc73ca67b5ac
parent 1349	ef26adb4e5b6
child 1469	fb9ccf06dfe8
permissions	-rwxr-xr-x