aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorherbelin2008-12-10 15:16:07 +0000
committerherbelin2008-12-10 15:16:07 +0000
commita35f6a25dcc00b3ea15adc4715cff0f98e537005 (patch)
tree15713e0c77e12e99a7ef4e053165e6f919865149 /scripts
parent70af80aad166bc54e4bbc80dfc9427cfee32aae6 (diff)
Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of
dp_zenon.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11663 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
0 files changed, 0 insertions, 0 deletions