From 14b5660ef1b8fb67bff60fa3ef3cbdb5ea2be718 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 31 Jan 2008 13:04:09 +0000
Subject: Move version check in case proof-site.el is loaded, not
 proof-site.elc

---
 generic/proof-site.el  | 21 +--------------------
 generic/proof-utils.el | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+), 20 deletions(-)

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 59a38a72..b9b65974 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -50,28 +50,9 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Emacs and PG versions
+;; PG version
 ;;
 
-(eval-and-compile 
-  (defun pg-emacs-version-cookie ()
-    (format (if (string-match "XEmacs" emacs-version) ; (featurep 'xemacs) gets optimised!
-		"XEmacs %d.%d" "GNU Emacs %d.%d")
-	    emacs-major-version emacs-minor-version))
-  
-  (defconst pg-compiled-for (eval-when-compile (pg-emacs-version-cookie))
-    "Version of Emacs we're compiled for (or running on, if interpreted)."))
-
-(if (or (not (boundp 'emacs-major-version))
-	(< emacs-major-version 21))
-    (error "Proof General is not compatible with Emacs %s" emacs-version))
-
-(unless (equal pg-compiled-for (pg-emacs-version-cookie))
-  (error 
-   (format 
-    "Proof General was compiled for %s but running on %s: please run \"make clean; make\""
-    pg-compiled-for (pg-emacs-version-cookie))))
-  
 (eval-and-compile
 ;; WARNING: do not edit next line (constant is edited in Makefile.devel)
   (defconst proof-general-version "Proof General Version 3.7pre080130. Released by da."
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 531b7fa0..24988a7c 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -15,6 +15,39 @@
 ;;
 
 (require 'proof-site)			; basic vars
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Give Emacs version mismatch error here.
+;;
+;; This file is loaded early, and may be first compiled file
+;; loaded if proof-site.el is loaded instead of proof-site.elc.
+;;
+(eval-and-compile 
+  (defun pg-emacs-version-cookie ()
+    (format (if (string-match "XEmacs" emacs-version) 
+		;; (featurep 'xemacs) gets optimised!!
+		"XEmacs %d.%d" "GNU Emacs %d.%d")
+	    emacs-major-version emacs-minor-version))
+  
+  (defconst pg-compiled-for 
+    (eval-when-compile (pg-emacs-version-cookie))
+    "Version of Emacs we're compiled for (or running on, if interpreted)."))
+
+(if (or (not (boundp 'emacs-major-version))
+	(< emacs-major-version 21))
+    (error "Proof General is not compatible with Emacs %s" emacs-version))
+
+(unless (equal pg-compiled-for (pg-emacs-version-cookie))
+  (error 
+   "Proof General was compiled for %s but running on %s: please run \"make clean; make\""
+   pg-compiled-for (pg-emacs-version-cookie)))
+
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;  
+
+
 (require 'proof-compat)		        ; for pg-defface-window-systems
 (require 'proof-config)			; config vars
 (require 'bufhist)			; bufhist 
-- 
cgit v1.2.3