doc-src/Ref/ref.tex
changeset 6572 e77641d2f4ac
parent 6571 971f238ef3ec
child 6592 c120262044b6
--- a/doc-src/Ref/ref.tex	Tue May 04 11:27:25 1999 +0200
+++ b/doc-src/Ref/ref.tex	Tue May 04 11:31:29 1999 +0200
@@ -1,8 +1,8 @@
 \documentclass[12pt]{report}
-\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,pdfsetup}
+\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup}
 
 %% $Id$
-%\includeonly{introduction}
+%%\includeonly{}
 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
 %%% to delete old ones:  \\indexbold{\*[^}]*}
 %% run    sedindex ref    to prepare index file