<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_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">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><div bgcolor="#FFFFFF"></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></div>