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 /lego | |
| parent | b50aa5058c361ac72a293c70b4ee82e7cd608279 (diff) | |
renamed proof-commands-regexp to proof-indent-commands-regexp, which
is less confusing);
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lego/lego.el b/lego/lego.el index 5b34d6bc..f7eafdbe 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -368,7 +368,7 @@ Checks the width in the `proof-goals-buffer'" proof-save-with-hole-regexp lego-save-with-hole-regexp proof-goal-with-hole-regexp lego-goal-with-hole-regexp proof-kill-goal-command lego-kill-goal-command - proof-commands-regexp (proof-ids-to-regexp lego-commands)) + proof-indent-commands-regexp (proof-ids-to-regexp lego-commands)) (lego-init-syntax-table) |