summaryrefslogtreecommitdiff
path: root/test-suite/misc/7704.sh
blob: 0ca2c97d244bf1b29fedfb4f16500c0ad1de5e07 (plain)
1
2
3
4
5
6
7
#!/usr/bin/env bash

set -e

export PATH=$BIN:$PATH

${coqtop#"$BIN"} -compile misc/aux7704.v