# HG changeset patch
# User wenzelm
# Date 1761499479 -3600
# Node ID c08765f8ceaf1c88a6daa11e486e8eb8fcb64f6a
# Parent  6f6062df9e05584450bb09bce14ecce973f592ec
proper message test (amending 9252ebcd1fb5);

diff -r 6f6062df9e05 -r c08765f8ceaf src/Tools/VSCode/extension/media/sledgehammer.js
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 17:12:31 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Sun Oct 26 18:24:39 2025 +0100
@@ -226,7 +226,7 @@
   window.addEventListener('message', event => {
     const message = event.data;
     if (message.command === 'status') {
-      spinner.classList.toggle('loading', message.message !== "Beendet");
+      spinner.classList.toggle('loading', message.message !== "Finished");
     }
     else if (message.command === 'provers') {
       set_history(message.history);