src/Pure/config.ML
changeset 80266 d52be75ae60b
parent 76058 d45a45eb1aee