<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Reviewing a PR just now, I'm reminded
that the logic I half-recalled to avoid empty serializations is
only for strings. Would it be worth changing [unit] serialization
to avoid empty serializations there, too?<br>
</div>
<div class="moz-cite-prefix"><br>
</div>
<div class="moz-cite-prefix">On 1/25/19 8:21 AM, Simon Van Casteren
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAC0+czrfSzNTz6tjVNZm471qUL-bHeeELCXcyOwisWAU9u-GFw@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div dir="ltr">
<div>
<div dir="auto">It doesn't happen often of course, since you
rarely use unit in a page or RPC function. How I ran into
it was actually via the now fixed bug
<div><a href="https://github.com/urweb/urweb/issues/117"
target="_blank" moz-do-not-send="true">https://github.com/urweb/urweb/issues/117</a>,
I made some ADT's that got around that bug by declaring
all constructors to have at least one parameter, unit if
nothing else. That came back to bite me now...</div>
<div><br>
</div>
<div>A page with this signature:</div>
<div><br>
</div>
<div>
<div><font face="monospace, monospace">val page: unit
-> string -> transaction page</font></div>
</div>
<div><br>
</div>
<div>Would be affected by the issue I described. This
obviously won't happen much outside of you making a
mistake (for example because first the function took
just a unit, then you added the string parameter), but
because it doesn't happen often and it's actually nginx
making the "mistake", I still thought it could help
someone out in the future!</div>
<div><br>
</div>
<div>Simon</div>
</div>
</div>
</div>
</div>
<div><br>
<div class="gmail_quote">
<div dir="ltr">On Fri, 25 Jan 2019 at 13:57, Adam Chlipala
<<a href="mailto:adamc@csail.mit.edu" target="_blank"
moz-do-not-send="true">adamc@csail.mit.edu</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">
<div bgcolor="#FFFFFF">
<div
class="gmail-m_4740153062521576460m_3892559965569003032moz-cite-prefix">Thanks
for sharing that wisdom! Somehow I remember making a
special effort to encode empty strings with underscores,
precisely to avoid this problem (though it was appearing
in Apache, if I recall correctly). Can you point us to
an example where it arises, in a URL that an Ur/Web app
generates itself?<br>
</div>
</div>
<div bgcolor="#FFFFFF">
<div
class="gmail-m_4740153062521576460m_3892559965569003032moz-cite-prefix"><br>
</div>
<div
class="gmail-m_4740153062521576460m_3892559965569003032moz-cite-prefix">On
1/25/19 5:13 AM, Simon Van Casteren wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">Hi,
<div><br>
</div>
<div>I just ran into an awful problem combining urweb
with nginx. By default, nginx by default merges
double slashes in urls, eg: <a
href="http://www.bla.com//users" target="_blank"
moz-do-not-send="true">http://www.bla.com//users</a>
becomes http//<a href="http://www.bla.com/users"
target="_blank" moz-do-not-send="true">www.bla.com/users</a>.
This can be a problem for UrWeb applications since a
double slash is actually how urweb encodes the unit
or () value. </div>
<div><br>
</div>
<div>The solution is to use the option: "merge_slashes
off". </div>
<div><br>
</div>
<div>It's not a bug in either application so I didnt
want me make an issue for it, but this could be
useful info for other people running Ur/Web programs
behind nginx...</div>
<div><br>
</div>
<div>Simon</div>
</div>
</blockquote>
</div>
</blockquote>
</div>
</div>
</blockquote>
</body>
</html>