# HG changeset patch
# User wenzelm
# Date 934806140 -7200
# Node ID ad69aa13ddf619c4b1497c0cf19f56dfe384c590
# Parent  012d8defdaa3b9d3d7e77a690be93005ce7f649e
bib;

diff -r 012d8defdaa3 -r ad69aa13ddf6 doc-src/System/Makefile
--- 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)
diff -r 012d8defdaa3 -r ad69aa13ddf6 doc-src/System/system.tex
--- 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}