| changeset 26291 | d01bf7b10c75 |
| parent 25845 | c448a5f15f31 |
| child 27605 | 2c281958e45d |
--- a/src/Pure/General/output.ML Sat Mar 15 22:07:31 2008 +0100 +++ b/src/Pure/General/output.ML Sat Mar 15 22:07:32 2008 +0100 @@ -111,7 +111,7 @@ val tolerate_legacy_features = ref true; fun legacy_feature s = - (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s); + (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s); fun no_warnings f = setmp warning_fn (K ()) f;