Merge branch 'main' into refactor

2023-10-24 11:39:50 +02:00
parent 787d010b6c 8e4c993bd7
commit 5c41d5c83c
1 changed files with 1 additions and 3 deletions
@@ -137,9 +137,7 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
    <div className="exercise-statement">
      {data?.descrText &&
        <Markdown>
-          {data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : "" // data?.descrText && "**Exercise**: "
-            + data?.descrText
-          }
+          {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + data?.descrText}
        </Markdown>
      }
      {data?.descrFormat && showLeanStatement &&