summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-09 15:47:48 +0000
committerGravatar tabarbe <unknown>2010-08-09 15:47:48 +0000
commitf20b120b5e42f6851b0afd787240d1813d2fbcbb (patch)
tree65c810c7cbaa11940e842298bef2db9e64805a1c /Test
parent378caef76d846b8a587de40d75ff0c903af095c3 (diff)
Boogie: That file should not have been in the depot, but rather be created locally
Diffstat (limited to 'Test')
-rw-r--r--Test/sanity/Output4
1 files changed, 0 insertions, 4 deletions
diff --git a/Test/sanity/Output b/Test/sanity/Output
deleted file mode 100644
index 72700e47..00000000
--- a/Test/sanity/Output
+++ /dev/null
@@ -1,4 +0,0 @@
-
-Boogie program verifier finished with 0 verified, 0 errors
-
-Dafny program verifier finished with 11 verified, 0 errors