Javascript suggestion: Better use `encodeURIComponent` than `encodeURI`

[hbghlyj]

Differences: encodeURI is used to encode a full URL. Whereas encodeURIComponent is used for encoding a URI component such as a query string.

So I think it is better to use encodeURIComponent than encodeURI in docs/run.html line 39

      var newl="?" + encodeURI(t).replace(/\$/g,'%24');

and line 49

	  document.location.search = "?" + encodeURI(t).replace(/\$/g,'%24');

..but it seems to make no difference

[davidcarlisle]

er yes I think in principle you are right, but I recall going through a few iterations here to get something that worked in a range of browsers so I'll leave this open for a bit to see if I can remember if this was a concious decision or not. If you find an example where you get a different result...

ah yes I see, it would make a difference if there is say an & in the latex

https://texlive.net/run?%5Cdocumentclass%7Barticle%7D%0A%5Cbegin%7Bdocument%7D%0Aa%20%5C&%20b%0A%5Cend%7Bdocument%7D

which leaves the & there unquoted but it doesn't actually matter as the form's post handler doesn't actually split up the query string on & note there is no ?file=... it's simply ?....

on the other hand I might want to extend things one day to allow query parameters in which case the suggested change would be needed.

I'll probably do this but not rush in to it, thanks for the suggestion.