aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar CJ Bell <cj@csail.mit.edu>2016-06-20 09:58:43 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-20 09:59:49 +0200
commitbef8d3ec1c1ea37b6867519fa7c9da80ccd6b3f6 (patch)
tree3211061e2de0fade418096bc9d9e179386b898df /configure.ml
parent3a4ba0659b7ed8072a7df5d2d978bf10194ff039 (diff)
LtacProf reports structured results (pr/209)
using a custom feedback message in response to "Show Ltac Profile."
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions