info manual: erase one useless file.
parent
e27bbbdb8c
commit
533e0cdd29
|
@ -84,7 +84,7 @@ info: files
|
||||||
-I ../cmds -I ../tutorials -I ../../styles -I ../texstuff \
|
-I ../cmds -I ../tutorials -I ../../styles -I ../texstuff \
|
||||||
../manual.inf -e macros.tex ../manual.tex
|
../manual.inf -e macros.tex ../manual.tex
|
||||||
cat manual.info.header infoman/ocaml.info.body > infoman/ocaml.info
|
cat manual.info.header infoman/ocaml.info.body > infoman/ocaml.info
|
||||||
cd infoman; rm -f ocaml.info.tmp; gzip -9 ocaml.info*
|
cd infoman; rm -f ocaml.info.tmp ocaml.info.body ; gzip -9 ocaml.info*
|
||||||
|
|
||||||
text: files
|
text: files
|
||||||
cd textman; \
|
cd textman; \
|
||||||
|
|
Loading…
Reference in New Issue