src/Pure/General/output.ML
changeset 80145 0eff7d113549
parent 73834 364bac6691de