Merge pull request #444 from ejgallego/fix_workspace_message

[workspace] Fix message about workspace detection
ejgallego · Mar 3, 2023 · 52ebcab · 52ebcab
2 parents 9c2d70e + 32db677
commit 52ebcab
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/CHANGES.md b/CHANGES.md
@@ -11,6 +11,8 @@
    #234)
  - Fix bug that prevented "Goal after tactic" from working properly
    (@ejgallego, #438, reported by David Ilcinkas)
+ - Message about workspace detection was printing the wrong file,
+   (@ejgallego, #444, reported by Alex Sanchez-Stern)
 
 # coq-lsp 0.1.6: Peek
 ---------------------

diff --git a/coq/workspace.ml b/coq/workspace.ml
@@ -252,7 +252,7 @@ let workspace_from_coqproject ~cmdline ~debug cp_file : t =
       }
   in
   let implicit = true in
-  let kind = Filename.concat (Sys.getcwd ()) "_CoqProject" in
+  let kind = cp_file in
   make ~cmdline ~implicit ~kind ~debug
 
 let workspace_from_cmdline ~debug ~cmdline =