diff options
| author | Pierre Courtieu | 2003-02-04 12:23:03 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2003-02-04 12:23:03 +0000 |
| commit | defde678caf25e8a5110934d0f72d11897135f22 (patch) | |
| tree | f50c4f3b2a49bc83bef66d2d37496cb805b3805b /html/feedback.php | |
| parent | 141e3000b9cd440b8408948d9ce6bd1b2cda7cab (diff) | |
Coq/pg: fixed a little bug with the "Print Hint" state preserving
command, which must not be matched by the state changing command
"Hint". I put "\\`Hint" in the keyword list, but I am not sure this is
the best way.
Diffstat (limited to 'html/feedback.php')
0 files changed, 0 insertions, 0 deletions