aboutsummaryrefslogtreecommitdiff
path: root/ci/simple-tests/.gitignore
diff options
context:
space:
mode:
authorErik Martin-Dorel2021-04-21 20:00:36 +0200
committerGitHub2021-04-21 20:00:36 +0200
commitb5c4c3a1423c7925194334d66c262054d6a6c4c5 (patch)
treee7878c97ece66bd7941e8f6019f70325de3f1bd1 /ci/simple-tests/.gitignore
parentd0acb626eba17023c55b002921870d60e48527a5 (diff)
parent82311da10ee3dfa6f29ddfb9225f9f05c29dca31 (diff)
Merge pull request #559 from hendriktews/omit-proofsHEADmaster
Add feature to omit complete opaque proofs
Diffstat (limited to 'ci/simple-tests/.gitignore')
-rw-r--r--ci/simple-tests/.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/ci/simple-tests/.gitignore b/ci/simple-tests/.gitignore
new file mode 100644
index 00000000..67f5cfcf
--- /dev/null
+++ b/ci/simple-tests/.gitignore
@@ -0,0 +1 @@
+*.success