From 1daef0d80f1b3cdf51fcfdc0e18c2fe9ed8d2c7e Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 25 Apr 2024 15:10:51 +0200 Subject: [PATCH] show exercise name even if no text present --- client/src/components/infoview/main.tsx | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 729600b..fc089fd 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -142,9 +142,12 @@ function ExerciseStatement({ data, showLeanStatement = false }) { if (!(data?.descrText || data?.descrFormat)) { return <> } return <>
- {data?.descrText && + {data?.descrText ? {(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})} + : data?.displayName && + + {`**${t("Theorem")}** \`${data?.displayName}\``} } {data?.descrFormat && showLeanStatement &&