diff --git a/Makefile.in b/Makefile.in
index af44687c..86b62fed 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -13,7 +13,7 @@ LDNAME=@LDNAME@
 LDNAME_VERSION=@LDNAME_VERSION@
 LDNAME_MAJOR=@LDNAME_MAJOR@
 
-all: doc
+all: @EXTRA_BUILD@
 	$(MAKE) -C src all || exit
 	@echo
 	@echo
diff --git a/configure b/configure
index 44627367..ccba88d1 100755
--- a/configure
+++ b/configure
@@ -41,6 +41,7 @@ PREFIX=${PREFIX:-"/usr/local"}
 LDNAME="libck.so"
 LDNAME_VERSION="libck.so.$VERSION"
 LDNAME_MAJOR="libck.so.$VERSION_MAJOR"
+EXTRA_BUILD='doc'
 
 OPTION_CHECKING=1
 
@@ -135,6 +136,7 @@ generate()
 	    -e "s#@LDNAME_VERSION@#$LDNAME_VERSION#g"		\
 	    -e "s#@PC_CFLAGS@#$PC_CFLAGS#g"			\
 	    -e "s#@GIT_SHA@#$GIT_SHA#g"			        \
+	    -e "s#@EXTRA_BUILD@#$EXTRA_BUILD#g"			\
 		$1 > $2
 }
 
@@ -160,6 +162,7 @@ generate_stdout()
 	echo "           LDFLAGS = $LDFLAGS"
 	echo "        SHARED_LIB = `expr $DISABLE_SHARED = 0`"
 	echo "        STATIC_LIB = `expr $DISABLE_STATIC = 0`"
+  echo "       EXTRA_BUILD = $EXTRA_BUILD"
 	echo "              GZIP = $GZIP"
 	echo "             CORES = $CORES"
 	echo "      POINTER_PACK = $POINTER_PACK_ENABLE"