blob: d22b9c8f7c7f1173072145f979207ca94e6a072c (
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" && jbuilder build @install )
echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
|
