diff options
| author | Pierre Courtieu | 2001-04-10 14:38:19 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2001-04-10 14:38:19 +0000 |
| commit | 021bed3d60eee84cea6099e22737accf37e3b21c (patch) | |
| tree | 01f26f27d967a547ce3a7d5475ec70910bd8d6f3 /html/index.php | |
| parent | 08506ce6b80ac8e1a7572dae20faeb0df2c0ad11 (diff) | |
Modification of proof-script-command-end-regexp to allow commands
ended by ".eof"
Diffstat (limited to 'html/index.php')
0 files changed, 0 insertions, 0 deletions