summaryrefslogtreecommitdiff
path: root/snapshots/coq-riscv/clean
diff options
context:
space:
mode:
Diffstat (limited to 'snapshots/coq-riscv/clean')
-rwxr-xr-xsnapshots/coq-riscv/clean13
1 files changed, 13 insertions, 0 deletions
diff --git a/snapshots/coq-riscv/clean b/snapshots/coq-riscv/clean
new file mode 100755
index 00000000..9b161fd2
--- /dev/null
+++ b/snapshots/coq-riscv/clean
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+if [ ! -d bbv ]; then
+ echo Run clean from the coq-riscv directory
+ exit 1
+fi
+
+set -ex
+rm -f sail/riscv/*.vo
+cd sail/lib/coq
+make clean
+cd ../../../bbv
+make clean