src/Pure/ProofGeneral/preferences.ML
changeset 28591 790d1863be28
parent 28587 52ec4c827ed4
child 29435 a5f84ac14609
--- 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;