equal
deleted
inserted
replaced
12 |
12 |
13 rcp index.html www4:.html-data/isabelle |
13 rcp index.html www4:.html-data/isabelle |
14 rcp Tools/*.gif www4:.html-data/isabelle/Tools |
14 rcp Tools/*.gif www4:.html-data/isabelle/Tools |
15 |
15 |
16 if ( "$*" == "" ) then |
16 if ( "$*" == "" ) then |
17 rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF LK Modal ZF \ |
17 rcp -r CCL CTT Cube FOL FOLP HOL HOLCF LCF Sequents ZF \ |
18 www4:.html-data/isabelle |
18 www4:.html-data/isabelle |
19 else |
19 else |
20 rcp -r $* www4:.html-data/isabelle |
20 rcp -r $* www4:.html-data/isabelle |
21 endif |
21 endif |
22 rsh www4 "chgrp -R isabelle .html-data/isabelle/*; chmod -R g+w .html-data/isabelle/*" |
22 rsh www4 "chgrp -R isabelle .html-data/isabelle/*; chmod -R g+w .html-data/isabelle/*" |