diff options
| author | Pierre Courtieu | 2004-02-19 12:16:03 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2004-02-19 12:16:03 +0000 |
| commit | acc38950cbf229bc6cdc1cc38138762b219e7b1a (patch) | |
| tree | 61300b98c799bff35fd05feaba966c59324445f4 /generic | |
| parent | b3311260c5fc24d7e8adfaa2617e0fd05d325122 (diff) | |
added some lines in holes short doc. And some abbrevs for coq.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/holes.el | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/generic/holes.el b/generic/holes.el index 6954eaa9..ab68925f 100644 --- a/generic/holes.el +++ b/generic/holes.el @@ -27,12 +27,12 @@ (switch-to-buffer-other-window "*doc holes*") (insert " -The highlighted # in your buffer are \"holes\", a powerful feature for -program editing. the character '#' is inserted to make empty holes -visible. If you don't replace \"#\"s by something else (see below), it -will be saved in the buffer's file. Highlighting of holes is made -without any interaction with the buffer's file. to delete a hole, -click with button 3 of your mouse. See the short documentation below +The highlighted # in your buffer are \"holes\", holes are a powerful +feature for program editing. the character '#' is inserted to make +empty holes visible. You can delete them like usual characters. If you +don't replace \"#\"s by something else (see below), it will be saved +in the buffer's file as usual '#' characters. To delete a hole, click +on it with button 3 of your mouse. See the short documentation below to learn how to use holes. HOLES |