From f17163e4895bdd6677da1616aafac0e5ee58c7d3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 15:34:34 +0000 Subject: [PATCH] ... --- helm/matita/matita.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 7521cb49f..7e4d747fa 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -90,6 +90,9 @@ TODO - riattaccare hbugs (brrr...) -> Zack GUI LOGICA + - tutte gli script che parsano (e.g. matitaclean, matitadep) debbono + processare la notazione per evitare errori di parsing (visibili ora + che e' stata committata la contrib list)! - la funzione alias_diff e' lentissima (anche se CSC l'ha accellerata di un fattore 3x) e puo' essere evitata: chi vuole aggiungere alias (la disambiguazione, il comando "alias" e l'add_obj) deve indicare -- 2.39.2