]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5868bef) | patch
- new handling of links
authorLuca Padovani <luca.padovani@unito.it>
Sat, 10 Nov 2001 19:16:54 +0000 (19:16 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Sat, 10 Nov 2001 19:16:54 +0000 (19:16 +0000)
commit75967c868f11708ad64e881dbe15a38718e441b7
tree3810419c719bb9c0eb86a8217eefd0250286982ctree | snapshot
parent5868bef6637af919fbb48a83c24268bb85bdef6acommit | diff
- new handling of links
- no more conflict between links and actions (links have precedence)
- cursors now handled by helmpot
- fixed problem with pot cursor
helm/helmpot/configure.in diff | blob | history
helm/helmpot/guiGTK.c diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.