<br> <div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I tried &#39;min&#39; and combinations with asterisks before and after and<br>
never got argmin as a result.<br></blockquote><div><br>On my (yesterday&#39;s) install, it is on the second page when searching for min.<br>I believe the search matches on partial strings too. <br><br>It&#39;s obviously not a perfect solution, e.g., there could be an option to list all the identifiers containing &quot;min&quot;, without duplicates, and then showing all module-variants of each identifier.<br>


A regexp-match on identifiers would be useful too sometimes.<br><br>Laurent<br></div></div></div>