src/Pure/System/message_channel.ML
changeset 83417 b51e4a526897
parent 80505 e3af424fdd1a