src/Pure/Tools/update_header.scala
changeset 75906 2167b9e3157a
parent 75394 42267c650205
--- a/src/Pure/Tools/update_header.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Tools/update_header.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -54,7 +54,7 @@
 
         for {
           spec <- specs
-          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+          file <- File.find_files(Path.explode(spec).file, file => File.is_thy(file.getName))
         } update_header(section, File.path(file))
       })
 }