diff options
Diffstat (limited to 'doc/newfaq/run.sh')
| -rwxr-xr-x | doc/newfaq/run.sh | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/newfaq/run.sh b/doc/newfaq/run.sh deleted file mode 100755 index 808d59b36..000000000 --- a/doc/newfaq/run.sh +++ /dev/null @@ -1,6 +0,0 @@ -#/bin/sh -coq-tex -n 72 -v -sl -small main.tex && latex main.v.tex && bibtex main.v && latex main.v.tex && latex main.v.tex && hevea -fix -nosymb main.v.tex - -# Commands for installation on pauillac -# scp main.v001.gif interval_discr.v pauillac.inria.fr:/net/pauillac/infosystems/www/coq/doc -# scp main.v.html pauillac.inria.fr:/net/pauillac/infosystems/www/coq/doc/faq.html |