diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-10 19:07:03 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-10 19:07:03 +0000 |
| commit | 52a7bbf10dab7d4f7f7bbdf9ddec08805693919c (patch) | |
| tree | 706bfefefeba6278b64eb5e1cabbe18d9db096ce /.gitignore | |
| parent | e2196880cfb406b56c829c7ed552107fa9dcb8b7 (diff) | |
Use the Makefile in test-suite/check
The output format is preserved, but not the dynamics (results are
showed all at once at the end). This script could be removed
altogether once the main Makefile (and daily bench) are fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12922 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions