docs generation back in; updates #134'

martukas · martukas · commit bf774d1772cc · 2018-01-21T20:42:53.000+01:00
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -230,7 +230,7 @@ node('docker') {
     // Delete workspace when build is done
     cleanWs()
 }
-/*
+
 node ("fedora") {
     // Delete workspace when build is done
     cleanWs()
@@ -294,4 +294,4 @@ node ("fedora") {
         }
     }
 }
-*/
+

Original file line number	Diff line number	Diff line change
`@@ -230,7 +230,7 @@ node('docker') {`
`230`	`230`	`// Delete workspace when build is done`
`231`	`231`	`cleanWs()`
`232`	`232`	`}`
`233`		`-/*`
	`233`	`+`
`234`	`234`	`node ("fedora") {`
`235`	`235`	`// Delete workspace when build is done`
`236`	`236`	`cleanWs()`
`@@ -294,4 +294,4 @@ node ("fedora") {`
`294`	`294`	`}`
`295`	`295`	`}`
`296`	`296`	`}`
`297`		`-*/`
	`297`	`+`