From fed6e45d564a7e2793540e1906e37fe8a8b2ea87 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 27 Oct 1999 13:01:36 +0000
Subject: tuned msg;

---
 generic/proof-script.el | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 5b7492a0..5b4a5123 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -448,7 +448,7 @@ proof assistant and Emacs is has a modified buffer visiting the file."
 	 (buffer (proof-file-to-buffer cfile)))
     (proof-debug (concat "Registering file " cfile 
 			 (if (member cfile proof-included-files-list)
-			     " (already registered, no action)." ".")))
+			     " (already registered, no action)" "")))
     (unless (member cfile proof-included-files-list)
       (and buffer
 	   (not informprover)
@@ -543,7 +543,7 @@ retracted using proof-auto-retract-dependencies."
 	 (concat "Unregistering file " cfile 
 		 (if (not (member cfile 
 				  proof-included-files-list))
-		     " (not registered, no action)." ".")))
+		     " (not registered, no action)" "")))
 	(if (member cfile proof-included-files-list)
 	    (progn
 	      (proof-auto-retract-dependencies cfile informprover)
@@ -1897,9 +1897,9 @@ This is intended as a value for proof-activate-scripting-hook"
 ;;
 
 (proof-define-assistant-command-witharg proof-find-theorems
- "Search for items containing a given constant."					
+ "Search for items containing given constants."
  proof-find-theorems-command
- "Find theorems containing the constant"
+ "Find theorems containing the constant(s)"
  (proof-shell-invisible-command arg))
 
 (proof-define-assistant-command-witharg proof-issue-goal
-- 
cgit v1.2.3