equal
deleted
inserted
replaced
150 } |
150 } |
151 |
151 |
152 def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = |
152 def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = |
153 { |
153 { |
154 val path = path0.expand.absolute |
154 val path = path0.expand.absolute |
155 if (!(path + Path.explode("etc/settings")).is_file && |
155 if (!check_dir(path)) error("Bad component directory: " + path) |
156 !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path) |
|
157 |
156 |
158 val lines1 = read_components() |
157 val lines1 = read_components() |
159 val lines2 = |
158 val lines2 = |
160 lines1.filter(line => |
159 lines1.filter(line => |
161 line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) |
160 line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) |