Commit 9c95b800 authored by Florent Lamiraux's avatar Florent Lamiraux Committed by Florent Lamiraux florent@laas.fr
Browse files

Download Makefile and config.sh from gepgitlab if in continuous integration.

parent df8f7bf2
......@@ -9,7 +9,7 @@ variables:
script:
- export INSTALL_DOCUMENTATION=OFF
- cp -r /clean_workspace $DEVEL_HPP_DIR
- /auto-install-hpp.sh --branch ${CI_COMMIT_REF_NAME} --target benchmark
- $CI_PROJECT_DIR/script/auto-install-hpp.sh --branch ${CI_COMMIT_REF_NAME} --gitrepo https://gepgitlab.laas.fr/humanoid-path-planner/hpp-doc/raw --target benchmark
artifacts:
paths:
- workspace
......
......@@ -34,6 +34,7 @@ case $HOST_DIST in
;;
esac
GITREPO="https://raw.githubusercontent.com/humanoid-path-planner/hpp-doc"
MAKE_TARBALL=false
TARGET=all
......@@ -51,6 +52,11 @@ do
--mktar)
MAKE_TARBALL=true
;;
--gitrepo)
shift
GITREPO=$1
echo "Will download Makefile and config.sh from $GITREPO"
;;
--show-dep)
echo "Will install"
echo "${APT_DEP}"
......@@ -71,6 +77,7 @@ do
--help)
echo "Options are"
echo "--branch: \tbranch which should be installed"
echo "--gitrepo: \trepository where to download makefile and config.sh"
echo "--mktar: \tmake tar balls after compilation"
echo "--show-dep: \tshow dependencies resolved by aptitude"
echo "--target TARGET: \tinstall TARGET (default: all)"
......@@ -116,8 +123,8 @@ mkdir --parents $DEVEL_HPP_DIR/src
mkdir --parents $DEVEL_HPP_DIR/install
# Get config script
wget -q -O $DEVEL_HPP_DIR/config.sh https://raw.githubusercontent.com/humanoid-path-planner/hpp-doc/${BRANCH}/doc/config/${CONFIG_FILE}
wget -q -O $DEVEL_HPP_DIR/src/Makefile https://raw.githubusercontent.com/humanoid-path-planner/hpp-doc/${BRANCH}/doc/Makefile
wget -q -O $DEVEL_HPP_DIR/config.sh ${GITREPO}/${BRANCH}/doc/config/${CONFIG_FILE}
wget -q -O $DEVEL_HPP_DIR/src/Makefile ${GITREPO}/${BRANCH}/doc/Makefile
source $DEVEL_HPP_DIR/config.sh
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment