phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix altTitle for backwards compatibility

Browse Source
This commit is contained in:
Jon Eugster
2023-12-14 22:06:53 +01:00
parent eaa214ec37
commit 03a370464b
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/inventory.tsx
+1 -1
View File
@@ -101,7 +101,7 @@ function InventoryItem({item, name, displayName, locked, disabled, newly, showDo
// Note: This is somewhat a hack as the statement of lemmas comes currently in the form
// `Namespace.statement_name (x y : Nat) : some type`
const title = locked ? "Not unlocked yet" :
disabled ? "Not available in this level" : item.altTitle.substring(item.altTitle.indexOf(' ') + 1)
disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
const [copied, setCopied] = useState(false)