aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ide/undo008.fake
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-06 14:04:06 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-09-06 14:04:06 +0000
commite614634b1fc2315410bd23ac19abc650186056c5 (patch)
tree0ef7566bdcf5c8c750176cf40257a4055de5d2a8 /test-suite/ide/undo008.fake
parentf402a7969a656eaf71f88c3413b991af1bbfab0a (diff)
test-suite/ide: misc improvement
- make clean really erases *.log - some missing \n at end of files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/ide/undo008.fake')
-rw-r--r--test-suite/ide/undo008.fake2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
index 799dc1ac1..1c46c1e87 100644
--- a/test-suite/ide/undo008.fake
+++ b/test-suite/ide/undo008.fake
@@ -15,4 +15,4 @@ INTERP Definition j := O.
INTERP assert True by trivial.
INTERP trivial.
INTERP Qed.
-INTERPRAW Check i. \ No newline at end of file
+INTERPRAW Check i.