src/Pure/Build/sessions.ML
changeset 81727 4ab59fef89ea
parent 79502 c7a98469c0e7
equal deleted inserted replaced
81726:27ba0fed2071 81727:4ab59fef89ea