src/Pure/General/README
changeset 11830 84dc8a2479d4
parent 9412 55e8230f5665