author | wenzelm |
Tue, 14 Oct 2008 15:45:46 +0200 | |
changeset 28591 | 790d1863be28 |
parent 28590 | d6f60fcb1b77 |
child 28592 | 824f8390aaa2 |
--- 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;