...

[helm.git] / helm / matita / matita.txt

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index c2510c9c3eff81b1dbf84f6274ce18e3d057a1aa..cbea07952c111bb17d5d4ee3ca6d967f0494568a 100644 (file)
--- 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