<div dir="ltr"><div class="gmail_default" style="font-family:courier new,monospace"><span style="font-family:arial,sans-serif">2018-04-18 8:28 GMT+02:00 Per Hedeland </span><span dir="ltr" style="font-family:arial,sans-serif"><<a href="mailto:per@hedeland.org" target="_blank">per@hedeland.org</a>></span><span style="font-family:arial,sans-serif">:</span><br></div><div class="gmail_quote"><div dir="ltr"><div style="font-family:courier new,monospace"><span style="font-family:arial,sans-serif">[...]</span></div><div class="gmail_extra"><div class="gmail_quote"><span class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span>
<br></span>
OK, so I looked at the code, and the change (see below) is so trivial<br>
that there is probably a good reason it doesn't already do that - I<br>
don't know what that reason might be though...<br></blockquote></span><div><br><div style="font-family:"courier new",monospace">​If someone accidentally mistypes a module name (to an other, existing module name), it might be unwise to load that different module​. Especially that the different module might have some code that executes at load time...</div></div><div><br><br></div></div></div></div>
</div><br></div>