# HG changeset patch
# User wenzelm
# Date 1223991946 -7200
# Node ID 790d1863be2863130fc6fbcc0eb81de70e28fe89
# Parent  d6f60fcb1b772ef864b36c8cb1109473ede0193f
adding preferences is now permissive;

diff -r d6f60fcb1b77 -r 790d1863be28 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;