adding preferences is now permissive;
authorwenzelm
Tue, 14 Oct 2008 15:45:46 +0200
changeset 28591 790d1863be28
parent 28590 d6f60fcb1b77
child 28592 824f8390aaa2
adding preferences is now permissive;
src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Tue Oct 14 15:45:45 2008 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Tue Oct 14 15:45:46 2008 +0200
@@ -194,7 +194,7 @@
     if cat <> cname then (cat, prefs)
     else
       if exists (fn {name, ...} => name = #name pref) prefs
-      then error ("Preference already exists: " ^ quote (#name pref))
+      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
       else (cat, pref :: prefs));
 
 end;