projects
/
tatoo.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
(from parent 2:
6bf7e46
)
Merge branch 'jit' of ssh://git.nguyen.vg/tatoo into jit
jit
author
Kim Nguyễn
<kim.nguyen@lri.fr>
Tue, 18 Apr 2017 12:53:58 +0000
(14:53 +0200)
committer
Kim Nguyễn
<kim.nguyen@lri.fr>
Tue, 18 Apr 2017 12:53:58 +0000
(14:53 +0200)
src/tree.ml
patch
|
blob
|
history
diff --git
a/src/tree.ml
b/src/tree.ml
index
2696707
..
a1cd6a1
100644
(file)
--- a/
src/tree.ml
+++ b/
src/tree.ml
@@
-157,5
+157,4
@@
sig
*)
val print_node : Format.formatter -> node -> unit
- val dispatch ('a -> 'b -> QName.t -> NodeSummary.t -> node -> node
end