diff options
| author | Pierre Courtieu | 2001-08-28 16:59:46 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2001-08-28 16:59:46 +0000 |
| commit | 242fa6a6b9e11d7c41537025e824ae546915c648 (patch) | |
| tree | eb4cbb45ff551fd530cbc3ad6f1bbd8d87d6ea6b /html/feedback.php | |
| parent | ae7413caac3728d2960ef4ffbe52cd24c3acc43e (diff) | |
Added something in the doc about coq-version-is-V7, and made the setting of
this variable more trustable with (concat coq-prog-name "-v").
Diffstat (limited to 'html/feedback.php')
0 files changed, 0 insertions, 0 deletions