From 0bf2756b85176d0bc04705bb3b10046a254f678b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr> Date: Mon, 9 Dec 2024 17:18:31 +0100 Subject: [PATCH] Add an error highlighting extension to better visualize errors in coq-lsp. --- Dockerfile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index e24fa60..71a188e 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,7 +1,8 @@ FROM inf110-workspace-base:latest -# Install the coq-lsp extension for code-server +# Install the coq-lsp extension for code-server and an extension that highlights errors in the code RUN code-server --install-extension ejgallego.coq-lsp +RUN code-server --install-extension usernamehw.errorlens # Install the Jupyter / Python extensions for code-server RUN code-server --install-extension ms-toolsai.jupyter -- GitLab