chore: change name of 'rebuild imports' button (#381)

leanprover · Dec 22, 2023 · 8d8c17e · 8d8c17e
1 parent 1711678
commit 8d8c17e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
@@ -119,8 +119,8 @@ export class LeanClient implements Disposable {
             return
         }
 
-        const message = `Imports of '${fileName}' are out of date and must be rebuilt.`
-        const input = 'Rebuild Imports'
+        const message = `Imports of '${fileName}' are out of date and must be rebuilt. Restarting the file will rebuild them.`
+        const input = 'Restart File'
         const choice = await window.showInformationMessage(message, input)
         if (choice !== input) {
             return