aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorGravatar Benjamin Gregoire <Benjamin.Gregoire@inria.fr>2015-03-26 14:21:13 +0100
committerGravatar Benjamin Gregoire <Benjamin.Gregoire@inria.fr>2015-03-26 14:41:26 +0100
commitc9074aa238e73bb932be67c67479b11bc95cd47a (patch)
tree02ed451f463c8973425568f4b34bcb2772ca1984 /kernel/cbytecodes.ml
parent2ef5fa7910e644d7eb39ee01024878a67086bd42 (diff)
add coqdep in distributed_exec, else make does not work.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions