# HG changeset patch
# User wenzelm
# Date 1343473918 -7200
# Node ID 4af9f312213812eecb4d3a6f04b01ccba637be24
# Parent  de82a584bc2a59d505ae057cc81978c5bbdb1eef
discontinued special treatment of Proof General;

diff -r de82a584bc2a -r 4af9f3122138 NEWS
--- a/NEWS	Sat Jul 28 13:01:48 2012 +0200
+++ b/NEWS	Sat Jul 28 13:11:58 2012 +0200
@@ -72,6 +72,11 @@
 without exception positions and advanced ML compiler/toplevel
 configuration.
 
+* Discontinued special treatment of Proof General -- no longer guess
+PROOFGENERAL_HOME based on accidental file-system layout.  Minor
+INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS
+settings manually, or use a Proof General version that has been
+bundled as Isabelle component.
 
 
 New in Isabelle2012 (May 2012)
diff -r de82a584bc2a -r 4af9f3122138 etc/settings
--- a/etc/settings	Sat Jul 28 13:01:48 2012 +0200
+++ b/etc/settings	Sat Jul 28 13:11:58 2012 +0200
@@ -165,23 +165,6 @@
 
 
 ###
-### Proof General / Emacs
-###
-
-# Proof General home, look in a variety of places
-PROOFGENERAL_HOME="$(choosefrom \
-  "$ISABELLE_HOME/contrib/ProofGeneral" \
-  "$ISABELLE_HOME/../ProofGeneral" \
-  "/usr/local/ProofGeneral" \
-  "/usr/share/ProofGeneral" \
-  "/opt/ProofGeneral" \
-  "")"
-
-PROOFGENERAL_OPTIONS=""
-#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
-
-
-###
 ### Rendering information
 ###