diff options
| author | letouzey | 2006-07-13 16:21:18 +0000 |
|---|---|---|
| committer | letouzey | 2006-07-13 16:21:18 +0000 |
| commit | d28d0d70a2c24bc4ecd3951ca58de84c3614e2b7 (patch) | |
| tree | 9e39e379506181493d51f6b7c4b73d00f3a0be36 /kernel/cbytecodes.ml | |
| parent | b10fc3d338314db1b3a4ee1097982cc8cf859e1b (diff) | |
Retrait du -noassert qui etait present en natif.
Ce -noassert empechait par exemple de s'apercevoir d'un echec actuel
dans la test-suite. Heureusement les paquets debian faits par Samuel
Mimram sont testés sur des tas d'archis, dont certaines en bytecode,
ce qui a permis de reperer le bug. Pour que de telles blagues ne se
reproduisent pas, il est essentiel que les asserts soient vérifiés y
compris en natif.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9049 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions