]> matita.cs.unibo.it Git - helm.git/commit
added decrease and increase font size fantafeature
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Jun 2005 11:55:21 +0000 (11:55 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Jun 2005 11:55:21 +0000 (11:55 +0000)
commit522bfe4fd22804ff7fb0013697721504003a6606
tree325c73916d644918e71cb33a299d1098ad920c1b
parent5d9c0b5cdda67ac1672b2e0dd83af7fb67a14a34
added decrease and increase font size fantafeature
helm/matita/buildTimeConf.ml.in
helm/matita/matita.conf.xml.sample
helm/matita/matita.glade
helm/matita/matita.ml
helm/matita/matitaGui.ml
helm/matita/matitaGui.mli
helm/matita/matitaMathView.ml
helm/matita/matitaMathView.mli
helm/matita/tests/record.ma