# HG changeset patch
# User wenzelm
# Date 932741668 -7200
# Node ID 55b80ec1927d7f20da2ea6dd725509d9a9e36845
# Parent  893e5a8a8d46c026513a4d1a131e7d8d9d5fa4a2
rail -a;

diff -r 893e5a8a8d46 -r 55b80ec1927d doc-src/Makefile.in
--- a/doc-src/Makefile.in	Fri Jul 23 16:52:45 1999 +0200
+++ b/doc-src/Makefile.in	Fri Jul 23 16:54:28 1999 +0200
@@ -9,7 +9,7 @@
 LATEX = latex
 PDFLATEX = pdflatex
 BIBTEX = bibtex
-RAIL = rail
+RAIL = rail -a
 SEDINDEX = ../sedindex
 FIXBOOKMARKS = perl -pi ../fixbookmarks.pl