aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh
blob: 991fb4a61d723e118d2e249e3747f95a97dab0a4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
#!/usr/bin/env bash

set -e

git clean -dfx

cat > _CoqProject <<EOT
-bypass-API
-I src/

./src/test_plugin.mllib
./src/test.ml4
./src/test.mli
EOT

mkdir src

cat > src/test_plugin.mllib <<EOT
Test
EOT

touch src/test.mli

cat > src/test.ml4 <<EOT
DECLARE PLUGIN "test"

let _ = Pre_env.empty_env
EOT

${COQBIN}coq_makefile -f _CoqProject -o Makefile

make VERBOSE=1