src/Tools/install_html.sh
author paulson
Mon, 02 Jun 1997 12:15:13 +0200
changeset 3385 f59e64fe4058
parent 2824 ec170ea5243e
permissions -rwxr-xr-x
New statement and proof of free_tv_subst_var in order to cope with new rewrite rules Un_insert_left, Un_insert_right
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1310
3d773439d844 removed buggy FTP scripts and replaced them by a script for transfer
clasohm
parents:
diff changeset
     1
#!/bin/csh
2824
wenzelm
parents: 2804
diff changeset
     2
# Executed from the Isabelle src directory, this script transfers all
1310
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
2824
wenzelm
parents: 2804
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
2824
wenzelm
parents: 2804
diff changeset
    22
rsh www4 "chgrp -R isabelle .html-data/isabelle/*; chmod -R g+w .html-data/isabelle/*"