equal
deleted
inserted
replaced
141 Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a))) |
141 Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a))) |
142 |
142 |
143 |
143 |
144 /* case-insensitive names */ |
144 /* case-insensitive names */ |
145 |
145 |
146 def check_case_insensitive(paths: List[Path]) |
146 def check_case_insensitive(paths: List[Path]): Unit = |
147 { |
147 { |
148 val table = |
148 val table = |
149 (Multi_Map.empty[String, String] /: paths)({ case (tab, path) => |
149 (Multi_Map.empty[String, String] /: paths)({ case (tab, path) => |
150 val name = path.expand.implode |
150 val name = path.expand.implode |
151 tab.insert(Word.lowercase(name), name) |
151 tab.insert(Word.lowercase(name), name) |