]> matita.cs.unibo.it Git - helm.git/commit
escape < in pango attrs
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 17 Aug 2008 14:38:40 +0000 (14:38 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 17 Aug 2008 14:38:40 +0000 (14:38 +0000)
commit37137e82f6e002d36c8052b506bf2d0a36fcd6de
tree6f05d1d227db7323ed6e45a9519d8898d5014f4c
parent5f3d564c7d5aa321a1a184ece75a5e1802a4fa2a
escape < in pango attrs
helm/software/matita/matitaAutoGui.ml