aboutsummaryrefslogtreecommitdiffhomepage
path: root/phox
diff options
context:
space:
mode:
authorGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2000-12-22 14:03:41 +0000
committerGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2000-12-22 14:03:41 +0000
commit34d69a349780126c8569aca64712de2c6a4cb616 (patch)
tree83f56fc87fe674036bbc4a06ec0bd99525c3b4f8 /phox
parentb63dd74e45d33d5493906b3c8caf00d0b84d8146 (diff)
*** empty log message ***
Diffstat (limited to 'phox')
-rw-r--r--phox/phox.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/phox/phox.el b/phox/phox.el
index e0274faf..8261cb03 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -142,7 +142,7 @@ phox-comments-regexp
(concat
"^"
phox-comments-regexp
- "\\(constraints\\|flag\\|goals\\|print\\(_sort\\)?\\|eshow\\|search\\|priority\\|depend\\)")
+ "\\(constraints\\|flag\\|goals\\|pri\\(nt\\(_sort\\)?\\|ority\\)\\|eshow\\|search\\|depend\\)")
proof-non-undoables-regexp
(concat
"^"