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