equal
deleted
inserted
replaced
39 } |
39 } |
40 |
40 |
41 def check_hg(root: Path) |
41 def check_hg(root: Path) |
42 { |
42 { |
43 Output.writeln("Checking " + root + " ...") |
43 Output.writeln("Checking " + root + " ...") |
44 Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check |
44 Isabelle_System.hg("--repository " + File.bash_path(root) + " root").check |
45 for { |
45 for { |
46 file <- Isabelle_System.hg("manifest", root).check.out_lines |
46 file <- Isabelle_System.hg("manifest", root).check.out_lines |
47 if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") |
47 if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") |
48 } check_file(root + Path.explode(file)) |
48 } check_file(root + Path.explode(file)) |
49 } |
49 } |