Trivial non-functional "bug" in the widget doc page

Stream: lean4

[Julian Berman]

This is trivial (so I'd send a PR presumably if it's welcome), and does not affect functionality in any way, but I suspect the example in the Hello World widget manual is not precisely what was intended -- specifically I bet someone wanted to concatenate the string in JS, because right now it will show just the string world!" if you don't pass a name, and will show the string julian! very excitedly if you do, as opposed to Hello world! and Hello julian!.

[Julian Berman]

(CC @David Thrane Christiansen I think? Though apologies if the ping isn't welcome.)

[David Thrane Christiansen]

A ping is just fine! But I think @Wojciech Nawrocki owns that page of docs.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ah yeah, that entire page is outdated. Let me update it.