src/Tools/install_html.sh
author nipkow
Mon, 25 Nov 1996 08:25:39 +0100
changeset 2221 39077a563a82
parent 2179 018906568ef0
child 2804 889d99613720
permissions -rwxr-xr-x
Replaced LK&Modal by Sequents
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
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
2179
018906568ef0 Now moves all Tool/*gif files.
nipkow
parents: 1469
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/*"