Fix my error: wget is run without root rights

This commit is contained in:
Laurent Rineau 2020-10-05 12:50:05 +02:00
parent da4acf4f0d
commit f88c0dec4a
1 changed files with 2 additions and 1 deletions

View File

@ -46,7 +46,8 @@ jobs:
set -x
sudo apt-get install -y graphviz ssh
sudo pip install lxml pyquery
wget --no-verbose -O /usr/bin/doxygen https://cgal.geometryfactory.com/~mgimeno/doxygen/build_1_8_13/bin/doxygen
wget --no-verbose -O doxygen_exe https://cgal.geometryfactory.com/~mgimeno/doxygen/build_1_8_13/bin/doxygen
sudo mv doxygen_exe /usr/bin/doxygen
sudo chmod +x /usr/bin/doxygen
git config --global user.email "maxime.gimeno@geometryfactory.com"
git config --global user.name "Maxime Gimeno"