equal
deleted
inserted
replaced
267 progress.echo(fail_msg); error(fail_msg) |
267 progress.echo(fail_msg); error(fail_msg) |
268 } |
268 } |
269 } |
269 } |
270 |
270 |
271 val session_base = |
271 val session_base = |
272 Sessions.session_base_info( |
272 Sessions.base_info( |
273 options, session_name, dirs = session_dirs, all_known = all_known).check_base |
273 options, session_name, dirs = session_dirs, all_known = all_known).check_base |
274 val resources = new VSCode_Resources(options, session_base, log) |
274 val resources = new VSCode_Resources(options, session_base, log) |
275 { |
275 { |
276 override def commit(change: Session.Change): Unit = |
276 override def commit(change: Session.Change): Unit = |
277 if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) |
277 if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) |