diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-05-27 19:24:05 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-05-27 19:24:05 +0000 |
| commit | 654813cfbde23c0855f1619d5894491dc1f7eec4 (patch) | |
| tree | 5748b5fca5ab3dd49407b3012432d7426add9044 /plastic | |
| parent | b50aa5058c361ac72a293c70b4ee82e7cd608279 (diff) | |
renamed proof-commands-regexp to proof-indent-commands-regexp, which
is less confusing);
Diffstat (limited to 'plastic')
| -rw-r--r-- | plastic/plastic.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el index 6eb8061c..4ba4586a 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -406,7 +406,7 @@ Given is the first SPAN which needs to be undone." proof-save-with-hole-regexp plastic-save-with-hole-regexp proof-goal-with-hole-regexp plastic-goal-with-hole-regexp proof-kill-goal-command plastic-kill-goal-command - proof-commands-regexp (proof-ids-to-regexp plastic-commands)) + proof-indent-commands-regexp (proof-ids-to-regexp plastic-commands)) (plastic-init-syntax-table) |