src/Pure/General/README
changeset 12249 dd9a51255855
parent 9412 55e8230f5665