aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/retroknowledge.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-09 18:40:14 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-09 18:40:14 +0200
commitba50753e9da60a23a40dedea59fb7f25e3ba4d15 (patch)
tree826df6950995c06af6a9dabc5dffee96285c938c /kernel/retroknowledge.mli
parent8770f0db6e16aaff27a14fd48eed2ae70338f3df (diff)
No need anymore for referring to xml directory in MLINCLUDES.
Diffstat (limited to 'kernel/retroknowledge.mli')
0 files changed, 0 insertions, 0 deletions