src/Pure/Thy/browser_info.ML
changeset 7484 9deae880cf74
parent 7409 f8ce7b832598
child 7572 6e6dafacbc28