src/Pure/System/gui_setup.scala
changeset 42230 594480d25aaa
parent 41381 77990a6cd558
child 43514 45cf8d5e109a
equal deleted inserted replaced
42229:1491b7209e76 42230:594480d25aaa