JS Console Error in inspect view
: TypeError: Cannot read properties of undefined (reading 'replace')
#1487
Labels
inspect view
: TypeError: Cannot read properties of undefined (reading 'replace')
#1487
I don't see any obvious failures from this, but when I click "sample" when viewing 2025-03-15T18-10-55+00-00_coq-to-lean_cVPifQF25ocKgzim9vbCb5.eval.tar.gz, I see in console
index.js:65751 TypeError: Cannot read properties of undefined (reading 'replace')
at htmlEscape (index.js:65988:21)
at HtmlFormatter.formatValue (index.js:65879:29)
at HtmlFormatter.format_added (index.js:65934:14)
at HtmlFormatter.recurse (index.js:65747:26)
at index.js:65762:16
at HtmlFormatter.forEachDeltaKey (index.js:65808:11)
at HtmlFormatter.formatDeltaChildren (index.js:65761:14)
at HtmlFormatter.format_node (index.js:65929:14)
at HtmlFormatter.recurse (index.js:65747:26)
at index.js:65762:16
The text was updated successfully, but these errors were encountered: