src/Pure/PIDE/document_editor.scala
Thu, 22 Dec 2022 15:23:26 +0100 wenzelm proper migrate_name between different kinds of Resources, notably for Windows;
less more (0) -1 tip