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;