<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><a moz-do-not-send="true"
href="https://github.com/urweb/urweb/commit/c4aba7a0befd9988ae032c5532790e5fabb321b9">Done</a>
now! Thanks for the suggestion.<br>
</p>
<div class="moz-cite-prefix">On 1/26/19 2:00 PM, Simon Van Casteren
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAC0+czoYKON979mzq_DkV7hxmBVH-ZJH51ZvtsniyFOOSEjXxA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">If it's not much work, I'd say yes. What I
mentioned won't happen often, but it was an extremely annoying
thing to track down.
<div><br>
</div>
<div>Simon</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">Op za 26 jan. 2019 om 19:33
schreef Adam Chlipala <<a href="mailto:adamc@csail.mit.edu"
moz-do-not-send="true">adamc@csail.mit.edu</a>>:<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_-4949381351408720010moz-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="gmail-m_-4949381351408720010moz-cite-prefix"><br>
</div>
<div class="gmail-m_-4949381351408720010moz-cite-prefix">On
1/25/19 8:21 AM, Simon Van Casteren wrote:<br>
</div>
<blockquote type="cite">
<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_-4949381351408720010gmail-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_-4949381351408720010gmail-m_4740153062521576460m_3892559965569003032moz-cite-prefix"><br>
</div>
<div
class="gmail-m_-4949381351408720010gmail-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>
</div>
_______________________________________________<br>
Ur mailing list<br>
<a href="mailto:Ur@impredicative.com" target="_blank"
moz-do-not-send="true">Ur@impredicative.com</a><br>
<a
href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur"
rel="noreferrer" target="_blank" moz-do-not-send="true">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Ur mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Ur@impredicative.com">Ur@impredicative.com</a>
<a class="moz-txt-link-freetext" href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a>
</pre>
</blockquote>
</body>
</html>