diff options
Diffstat (limited to 'build-aux/Jenkinsfile.mini')
| -rw-r--r-- | build-aux/Jenkinsfile.mini | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/build-aux/Jenkinsfile.mini b/build-aux/Jenkinsfile.mini index c765fc958..115365109 100644 --- a/build-aux/Jenkinsfile.mini +++ b/build-aux/Jenkinsfile.mini @@ -89,7 +89,7 @@ pipeline { ''' sh './configure --with-curl' sh 'make couch' - // sh 'make fauxton' + sh 'make fauxton' sh 'make docs' sh 'make dist' sh 'chmod -R a+w * .' |