contrib/ci.inria.fr: add developers documentation in stash

contrib/ci.inria.fr/Jenkinsfile-basic

@@ -44,12 +44,13 @@ pipeline
 					}
 					stash includes: "${env.tarballgz}", name: 'tarballgz'
 					stash includes: "starpu.pdf", name: 'doc'
+					stash includes: "starpu_dev.pdf", name: 'doc_dev'
 					// Stash those scripts because they are not in make dist
 					dir('contrib/ci.inria.fr')
 					{
 						stash includes: "job-1-check.sh", name: 'script-unix-check'
 					}
-					archiveArtifacts artifacts: "${env.tarballgz},starpu.pdf", fingerprint: true, onlyIfSuccessful: true
+					archiveArtifacts artifacts: "${env.tarballgz},starpu.pdf,starpu_dev.pdf", fingerprint: true, onlyIfSuccessful: true
 					deleteDir()
 
 				}

contrib/ci.inria.fr/job-0-tarball.sh

@@ -26,5 +26,6 @@ make V=1
 make dist
 cp *gz ..
 cp doc/doxygen/starpu.pdf ..
+cp doc/doxygen_dev/starpu_dev.pdf ..
 make clean