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