blob: 1a9a26843cc5a6d58740ff0879a7682a8139deb5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
git_download pidetop
# Travis / Gitlab have different filesystem layout due to use of
# `-local`. We need to improve this divergence but if we use Dune this
# "local" oddity goes away automatically so not bothering...
if [ -d "$COQBIN/../lib/coq" ]; then
COQLIB="$COQBIN/../lib/coq/"
else
COQLIB="$COQBIN/../"
fi
( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install )
echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
|
