sed -i 's|https://gitlab.inria.fr/learninglab/|https://learninglab.gitlabpages.inria.fr/|g' ${file%.*}.html;
sed -i "s|<body>|<body>The <a href='https://gitlab.inria.fr/learninglab/mooc-rr/mooc-rr-ressources/blob/master/$file'>original version of this document is available on gitlab</a>.|g" ${file%.*}.html;