src/Pure/Tools/jedit.ML
changeset 65631 ee917f172912
parent 63681 d2448471ffba
child 66670 e5188cb1c3d8
equal deleted inserted replaced
65630:c41bbf657310 65631:ee917f172912