src/Pure/Tools/update_header.scala
changeset 68994 d961e11e0e87
parent 62836 98dbed6cfa44
child 72763 3cc73d00553c
--- a/src/Pure/Tools/update_header.scala	Thu Sep 13 16:30:07 2018 +0200
+++ b/src/Pure/Tools/update_header.scala	Thu Sep 13 21:18:43 2018 +0200
@@ -56,6 +56,6 @@
       for {
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_header(section, Path.explode(File.standard_path(file)))
+      } update_header(section, File.path(file))
     })
 }