From 742fe586cf81bde132d0389f70c5c459eb144860 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 11 Jan 2001 19:57:52 +0000
Subject: fixed format strings in message, error, etc.

---
 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 d25e83f5..938fb73b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1124,7 +1124,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
       (let (nam gspan next)
 
 	;; Try to set the name of the theorem from the save
-	(message cmd)
+	(message "%s" cmd)
 
 	(and proof-save-with-hole-regexp
 	     (proof-string-match proof-save-with-hole-regexp cmd)
@@ -1132,7 +1132,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 		   (if (stringp proof-save-with-hole-result)
 		       (replace-match proof-save-with-hole-result nil nil cmd)
 		     (match-string proof-save-with-hole-result cmd))))
-	(message nam)
+	(message "%s" nam)
 	;; Search backwards for first goal command, 
 	;; deleting spans along the way.
 	(setq gspan span)
@@ -1151,7 +1151,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	;; If the name isn't set, try to set it from the goal. 
 	  (unless nam
 	    (let ((cmdstr (span-property gspan 'cmd)))
-	      (message cmdstr)
+	      (message "%s" cmdstr)
 	      (and proof-goal-with-hole-regexp
 		   (proof-string-match proof-goal-with-hole-regexp cmdstr)
 		   (setq nam 
@@ -1295,7 +1295,7 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	  ;; Try to set a name from the goal
 	  ;; (useless for provers like Isabelle)
 	  (let ((cmdstr (span-property gspan 'cmd)))
-	    (message cmdstr)
+	    (message "%s" cmdstr)
 	    (and proof-goal-with-hole-regexp
 		 (proof-string-match proof-goal-with-hole-regexp cmdstr)
 		 (setq nam 
-- 
cgit v1.2.3