diff -r 6ed5fe0ea387 -r 51eaad3a817b doc/Makefile
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/Makefile	Tue Dec 18 10:56:09 2007 +0100
@@ -0,0 +1,2 @@
+all:
+	$(MAKE) -C ..