# HG changeset patch
# User wenzelm
# Date 1599825262 -7200
# Node ID 8c5b8d7999bd0218bcd8a14e41301787d8a212fa
# Parent  1b01c626a44146ac6b12853d73f79d96d66bd1d0
more checks;

diff -r 1b01c626a441 -r 8c5b8d7999bd src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Fri Sep 11 12:56:01 2020 +0200
+++ b/src/Pure/Admin/check_sources.scala	Fri Sep 11 13:54:22 2020 +0200
@@ -18,7 +18,12 @@
     if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
       Output.warning("Illegal file-name on Windows" + Position.here(file_pos))
 
-    val content = File.read(path)
+    val bytes = Bytes.read(path)
+    val content = bytes.text
+
+    if (Bytes(content) != bytes) {
+      Output.warning("Bad UTF8 encoding" + Position.here(file_pos))
+    }
 
     for { (line, i) <- split_lines(content).iterator.zipWithIndex }
     {