From 9bb46a47cf4c1fa3994f0902391a4a90ec779d75 Mon Sep 17 00:00:00 2001
From: Olaf Bergmann <bergmann@tzi.org>
Date: Fri, 23 Jul 2010 18:20:20 +0200
Subject: [PATCH] target for building documentation does not work yet

---
 Makefile | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Makefile b/Makefile
index 399e0e9f..39aa5ba3 100644
--- a/Makefile
+++ b/Makefile
@@ -47,7 +47,6 @@ dist:
 	test -d $(DISTDIR)/$(examples) || mkdir $(DISTDIR)/$(examples)
 	cp $(FILES) $(DISTDIR)
 	$(MAKE) -C $(examples) dist DISTDIR=../$(DISTDIR)/$(examples)
-	$(MAKE) -C $(doc) dist DISTDIR=../$(DISTDIR)/$(doc)
 	tar czf $(DISTDIR).tar.gz $(DISTDIR)
 
 .gitignore: