From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Mar 2003 11:56:20 +0000 (+0000)
Subject: Bug introduced: the alias combo-box now accepts multiple selections (but
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=6c46e2f25042f33cb6af02701bc18cb9987d4ee4

Bug introduced: the alias combo-box now accepts multiple selections (but
use just the last selected item).
---

diff --git a/helm/searchEngine/html/aliaslist.html b/helm/searchEngine/html/aliaslist.html
index 2b5c54163..60c38cf72 100644
--- a/helm/searchEngine/html/aliaslist.html
+++ b/helm/searchEngine/html/aliaslist.html
@@ -71,7 +71,7 @@ alias
 <input name="idi" type=text size="15">
 <input name="uri" type=text size="45" value="cic:/"><br>
 <input type=submit value="add alias"><input type=button value="delete selected" onClick="rimuovialias()";><br>
-<select name="elenco" size=7>
+<select name="elenco" multiple size=7>
 <script language=Javascript> listalias(); document.aliaslist.idi.focus(); </script>
 </select>
 <br>