From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 Jul 2005 12:25:38 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_7_2~66
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e0166342ff75d4186e0251a348174eccc6d380b6;p=helm.git

...
---

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index c2510c9c3..cbea07952 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -77,6 +77,8 @@ TODO
     Il problema di questa soluzione e' che rallenta in maniera significativa
     l'esecuzione degli script. DOMANDA: quanto costano le fasi di
     fetch/decode/execute delle linee dello script?
+    Una possibile alternativa e' avere alias "soft": se la disambiguazione
+    fallisce gli alias soft vengono ripuliti e si riprova.
   - matitamake foo/a.ma non funziona; bisogna chiamarlo con
     matitamake /x/y/z/foo/a.ma
   - notazione -> Luca e Zack