From e0166342ff75d4186e0251a348174eccc6d380b6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 Jul 2005 12:25:38 +0000
Subject: [PATCH] ...

---
 helm/matita/matita.txt | 2 ++
 1 file changed, 2 insertions(+)

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
-- 
2.39.2