diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci/jobs/gcc5_h_pugi.sh | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/tools/ci/jobs/gcc5_h_pugi.sh b/tools/ci/jobs/gcc5_h_pugi.sh deleted file mode 100755 index de392c73e..000000000 --- a/tools/ci/jobs/gcc5_h_pugi.sh +++ /dev/null @@ -1,29 +0,0 @@ -#!/bin/bash - -export CC=gcc-5 -export CXX=g++-5 - -if [ "$NEWCC" != "" ]; then - export CC="$NEWCC" -fi -if [ "$NEWCXX" != "" ]; then - export CXX="$NEWCXX" -fi - -export LOGFILE=gcc5_h.log - -source ./tools/ci/scripts/init.sh - -do_init - -cd src -export dir=$(pwd) -export includes="-I$dir -I/usr/include -I/usr/include/libxml2" - -run_h $* - -cd .. - -source ./tools/ci/scripts/exit.sh - -exit 0 |