--- a/doc-src/System/Makefile Mon Aug 16 11:53:18 1999 +0200
+++ b/doc-src/System/Makefile Mon Aug 16 14:22:20 1999 +0200
@@ -13,13 +13,15 @@
NAME = system
FILES = system.tex basics.tex misc.tex fonts.tex present.tex \
- ../iman.sty ../extra.sty
+ ../iman.sty ../extra.sty ../manual.bib
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES) isabelle.eps
touch $(NAME).ind
$(LATEX) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(LATEX) $(NAME)
$(LATEX) $(NAME)
$(SEDINDEX) $(NAME)
$(LATEX) $(NAME)
@@ -29,6 +31,8 @@
$(NAME).pdf: $(FILES) isabelle.pdf
touch $(NAME).ind
$(PDFLATEX) $(NAME)
+ $(BIBTEX) $(NAME)
+ $(PDFLATEX) $(NAME)
$(PDFLATEX) $(NAME)
$(SEDINDEX) $(NAME)
$(PDFLATEX) $(NAME)
--- a/doc-src/System/system.tex Mon Aug 16 11:53:18 1999 +0200
+++ b/doc-src/System/system.tex Mon Aug 16 14:22:20 1999 +0200
@@ -32,6 +32,11 @@
\include{fonts}
\include{present}
+\begingroup
+ \bibliographystyle{plain} \small\raggedright\frenchspacing
+ \bibliography{../manual}
+\endgroup
+
\input{system.ind}
\end{document}