]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f3d564) | patch
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
tree6f05d1d227db7323ed6e45a9519d8898d5014f4ctree | snapshot
parent5f3d564c7d5aa321a1a184ece75a5e1802a4fa2acommit | diff
escape < in pango attrs
helm/software/matita/matitaAutoGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.