src/Pure/General/README
changeset 14099 55d244f3c86d
parent 9412 55e8230f5665