diff -r 0887d0dd3210 -r c04bbfe71cef doc-src/IsarAdvanced/Makefile.in
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Makefile.in	Thu Oct 12 08:10:23 2006 +0200
@@ -0,0 +1,13 @@
+# $Id$
+#
+
+include ../../Makefile.in
+
+SEDINDEX = ../../sedindex
+FIXBOOKMARKS = perl -pi ../../fixbookmarks.pl
+
+isabelle_isar.eps:
+	test -r isabelle_isar.eps || ln -s ../../gfx/isabelle_isar.eps .
+
+isabelle_isar.pdf:
+	test -r isabelle_isar.pdf || ln -s ../../gfx/isabelle_isar.pdf .