From d6882b57b9e5af98d734b0d79ed8573cacb25da7 Mon Sep 17 00:00:00 2001
From: sylvain tricot <sylvain.tricot@univ-rennes1.fr>
Date: Mon, 27 Sep 2021 14:17:25 +0200
Subject: [PATCH] Tried to fix the broken 'syncing website' stage.

This last stage is not working due to permission
issues on the server side. I tried to just update
existing files instead of removing everything and
copying new files. Let's see...
---
 Jenkinsfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index 11f99e8..9292a38 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -14,7 +14,7 @@ pipeline {
         stage('Syncing website...') {
             steps {
 		// echo 'Syncing website...'
-		sh 'rm -rf $HOME/www/*'
+		// sh 'rm -rf $HOME/www/*'
                 sh 'cp -a ./doc/build/html/* $HOME/www/'
             }
         }