aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/search.mli
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-17 22:39:26 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-17 22:39:26 +0000
commita4b676747b6d0390b882f1fcf8f3c394e4b916c6 (patch)
tree54f44e64a4395a345d634b943e6774d43ca14df8 /toplevel/search.mli
parent092525e3a71a59292e219492774a5aef21856518 (diff)
Makefile.build: CONFIG is now in clib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15909 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/search.mli')
0 files changed, 0 insertions, 0 deletions