Closed stefan-hoeck closed 12 months ago
As mentioned on discord, in the pack.toml file copied from the installation bash script, the (commented-out) list of apps to be installed automatically still contains the old name of the idris2-lsp application. This is fixed with this PR.
pack.toml
idris2-lsp
As mentioned on discord, in the
pack.toml
file copied from the installation bash script, the (commented-out) list of apps to be installed automatically still contains the old name of theidris2-lsp
application. This is fixed with this PR.