equal
deleted
inserted
replaced
210 { |
210 { |
211 progress.echo(fail_msg); error(fail_msg) |
211 progress.echo(fail_msg); error(fail_msg) |
212 } |
212 } |
213 } |
213 } |
214 |
214 |
215 val base = Build.session_base(options, false, session_dirs, session_name) |
215 val base = Build.session_base(options, session_name, session_dirs) |
216 val resources = new VSCode_Resources(options, base, log) |
216 val resources = new VSCode_Resources(options, base, log) |
217 { |
217 { |
218 override def commit(change: Session.Change): Unit = |
218 override def commit(change: Session.Change): Unit = |
219 if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) |
219 if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) |
220 delay_load.invoke() |
220 delay_load.invoke() |