aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc/quick-include.sh
blob: e60fb48bca8f2284d4bf3a08c5143cc3bf69842c (plain)
1
2
3
4
5
#!/bin/sh
set -e

$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file1.v
$coqc -R misc/quick-include/ QuickInclude -vio misc/quick-include/file2.v