]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ad10eb3) | patch
removing (only from the interface) functions related to ligatures that now live in...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 Jan 2009 16:07:48 +0000 (16:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 Jan 2009 16:07:48 +0000 (16:07 +0000)
commit279b11c00cdaacb4858e1c8dc6d05ea631bc1358
tree7e75b80382d03bd5264ce495afcf8641af55d4a0tree | snapshot
parentad10eb3697233a2e16b9f32fabe0595c0575f34acommit | diff
removing (only from the interface) functions related to ligatures that now live in the GUI
helm/software/components/content_pres/cicNotationLexer.ml diff | blob | history
helm/software/components/content_pres/cicNotationLexer.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.