<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">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">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">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">http://www.bla.com//users</a>
                    becomes http//<a href="http://www.bla.com/users" target="_blank">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">Ur@impredicative.com</a><br>
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br>
</blockquote></div>