src/Pure/General/README
changeset 13630 a013a9dd370f
parent 9412 55e8230f5665