undo == true

hhu-adam · Jul 13, 2024 · 99ee38b · 99ee38b
1 parent 1a13d52
commit 99ee38b
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/vscode-lean4/src/diagnostics/setupNotifs.ts b/vscode-lean4/src/diagnostics/setupNotifs.ts
@@ -131,7 +131,7 @@ export async function displaySetupWarning(
     if (!shouldShowSetupWarnings()) {
         return 'Warning'
     }
-    if (options.modal == true) {
+    if (options.modal) {
         const choice = await displayModalWarning(message)
         return choice === 'Proceed' ? 'Warning' : 'Fatal'
     }
@@ -169,7 +169,7 @@ export async function displaySetupWarningWithOutput(
     if (!shouldShowSetupWarnings()) {
         return 'Warning'
     }
-    if (options.modal == true) {
+    if (options.modal) {
         const choice = await displayModalWarningWithOutput(message)
         return choice === 'Proceed' ? 'Warning' : 'Fatal'
     }
@@ -184,7 +184,7 @@ export async function displaySetupWarningWithSetupGuide(
     if (!shouldShowSetupWarnings()) {
         return 'Warning'
     }
-    if (options.modal == true) {
+    if (options.modal) {
         const choice = await displayModalWarningWithSetupGuide(message)
         return choice === 'Proceed' ? 'Warning' : 'Fatal'
     }