Index: Jenkinsfile
===================================================================
--- Jenkinsfile	(revision 738cf8f3cf44716f347c8634dc13e02d0c982bcd)
+++ Jenkinsfile	(revision b2b039d9772b7f152f58bfc5777b2f070864bed5)
@@ -70,5 +70,7 @@
 
 def doc_build() {
-	build_stage 'Documentation'
+	stage 'Documentation'
+
+		status_prefix = 'Documentation'
 
 		dir ('doc/user') {