doc-src/IsarOverview/Makefile

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarOverview/Makefile	Mon May 12 12:12:19 2003 +0200
@@ -0,0 +1,22 @@
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+
+## dependencies
+
+dvi:
+	cd Isar/document; make dvi
+
+pdf:
+	cd Isar/document; make pdf
+
+clean:
+	cd Isar/document; make clean
+
+mrproper:
+	rm -f *.pdf *.dvi
+	cd Isar/document; make mrproper