aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/trac
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-24 13:02:12 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-24 13:02:12 +0000
commit6ba98422a95a799778378ecf7e34febc6577fa3b (patch)
tree2a287b720320ac8faf26dbf81073e5d4ea62e27e /etc/trac
parent88bef988d16cc4da0033ba2c0e4c9a6573c671dd (diff)
proof-script-command-end-regexp: allow any non-letter after a period
to terminate a command, fixing #296 (and hopefully not messing up other cases).
Diffstat (limited to 'etc/trac')
-rw-r--r--etc/trac/trac-296.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/etc/trac/trac-296.v b/etc/trac/trac-296.v
index ac0e223f..4ac6a676 100644
--- a/etc/trac/trac-296.v
+++ b/etc/trac/trac-296.v
@@ -1,3 +1,6 @@
(* PG accepts this as valid though it isn't;
see http://proofgeneral.inf.ed.ac.uk/trac/ticket/296 *)
Check nat.&!&*\:,.:<*&!)@)$.
+
+(* How should this one parse? *)
+Check 0.99.