doc-src/System/system.tex
changeset 8828 5be2d1745c61
parent 7882 52fb3667f7df
child 9695 ec7d7f877712
--- a/doc-src/System/system.tex	Mon May 08 11:13:11 2000 +0200
+++ b/doc-src/System/system.tex	Mon May 08 11:13:28 2000 +0200
@@ -35,6 +35,6 @@
   \bibliography{../manual}
 \endgroup
 
-\input{system.ind}
+\printindex
 
 \end{document}