<div dir="ltr"><div>Adam, <br></div><div><br></div><div>Yes, I've noticed ignored `onload` on  tags other than `body`. <br></div><div><br></div><div>It would be good to have a type error or allowing it more broadly.</div><div><br></div><div>Aistis<br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 22, 2018 at 11:41 AM Adam Chlipala <<a href="mailto:adamc@csail.mit.edu">adamc@csail.mit.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
  
    
  
  <div text="#000000" bgcolor="#FFFFFF">
    <div class="m_-56428009462031281moz-cite-prefix">Belated follow-up on this remark: now
      that I look at the types from the standard library, I see that
      'onload' is statically disallowed for <div> and indeed most
      other tags.  Is that what you meant?  It could be reasonable to
      add 'onload' more widely, but currently including it for most tags
      should not have 'no effect'.  Instead, it should trigger type
      error messages!<br>
    </div>
    <div class="m_-56428009462031281moz-cite-prefix"><br>
    </div>
    <div class="m_-56428009462031281moz-cite-prefix">On 7/5/18 2:05 PM, Adam Chlipala wrote:<br>
    </div>
    <blockquote type="cite">
      
      On 07/05/2018 01:43 PM, Fabrice Leal wrote:<br>
      <blockquote type="cite">
        <div dir="ltr"><span style="color:rgb(0,0,0);white-space:pre-wrap">I found out too late for my own good that onload only works for <body>, placing it in a <div> as no effect</span></div>
      </blockquote>
      <br>
      Oh, I didn't realize that some event attribute was systematically
      ignored.  That might qualify as a bug!</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>