From acc38950cbf229bc6cdc1cc38138762b219e7b1a Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 19 Feb 2004 12:16:03 +0000
Subject: added some lines in holes short doc. And some abbrevs for coq.

---
 generic/holes.el | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'generic')

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
-- 
cgit v1.2.3