add git remote branch to upload odoc

serban-nicusor-toptal · web-flow · commit b0f2bd3de4e1 · 2021-11-03T01:14:30.000+01:00
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -658,6 +658,7 @@ pipeline {
 
                 // Checkout gh-pages as a test so we build docs from this branch
                 runShell("""
+                    git remote set-branches --add origin gh-pages
                     git checkout --track  origin/gh-pages
                     git checkout master
                 """)
@@ -702,4 +703,4 @@ pipeline {
           script {utils.mailBuildResults()}
         }
     }
-}
+}

Original file line number	Diff line number	Diff line change
`@@ -658,6 +658,7 @@ pipeline {`
`658`	`658`
`659`	`659`	`// Checkout gh-pages as a test so we build docs from this branch`
`660`	`660`	`runShell("""`
	`661`	`+ git remote set-branches --add origin gh-pages`
`661`	`662`	`git checkout --track origin/gh-pages`
`662`	`663`	`git checkout master`
`663`	`664`	`""")`
`@@ -702,4 +703,4 @@ pipeline {`
`702`	`703`	`script {utils.mailBuildResults()}`
`703`	`704`	`}`
`704`	`705`	`}`
`705`		`-}`
	`706`	`+}`