aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc
Commit message (Collapse)AuthorAge
* add test for #7595Gravatar Ralf Jung2018-06-07
|
* Merge PR #7484: Fix non-portable shebang in test-suite.Gravatar Enrico Tassi2018-05-16
|\
* \ Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵Gravatar Gaëtan Gilbert2018-05-14
|\ \ | | | | | | | | | symlink from repo
| * | Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repoGravatar Ralf Jung2018-05-13
| | | | | | | | | | | | Fixes #7065
| | * Fix non-portable shebang in test-suite.Gravatar Théo Zimmermann2018-05-11
| |/ |/|
* | test for coqc -oGravatar Enrico Tassi2018-05-09
|/
* Improve shell scriptsGravatar zapashcanon2018-04-05
|
* Adding a test for utf8 characters in directory names.Gravatar Hugo Herbelin2017-09-13
|
* Remove trailing CR before diff in output and misc tests.Gravatar Maxime Dénès2017-07-20
|
* Should fix a false negative reported by deps-order.sh.Gravatar Hugo Herbelin2017-06-21
| | | | | | | The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
* A stronger test that #use"include";; works well.Gravatar Hugo Herbelin2017-06-11
|
* Moving code for miscellaneous tests to specific files.Gravatar Hugo Herbelin2017-05-10
| | | | | | | | | | | | | | | | | | The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
* Adding tests for testing exit status and #use"include".Gravatar Hugo Herbelin2017-05-10
|
* Cleaning old untested not any more interesting testing files.Gravatar Hugo Herbelin2017-05-10
|
* test-suite: test checking of libraries checksum.Gravatar Maxime Dénès2016-07-04
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
| | | | | | | Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
* test suite update after r14808Gravatar pboutill2011-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a test for sorting all universes of stdlibGravatar glondu2011-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inGravatar herbelin2010-09-18
| | | | | | coqdep since it is now deterministic (later -R's overwriting former ones). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing xml theory file export (was not consistent with coqdoc fileGravatar herbelin2009-11-26
naming heuristic). Added a corresponding test. Note: maybe should the generated .v file for exporting the theory be made of a valid ident if ever coqdoc eventually follows coq convention: currently it has name foo.theory.v which is not coqc-compilable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12543 85f007b7-540e-0410-9357-904b9bb8a0f7