aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-04-07 19:36:55 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-04-07 19:38:48 +0200
commit7d3ce4012a53b123dac95381bf46aac65f865d69 (patch)
treee408eff343dce996f1f2bd267d78e8f2c61b1c72 /parsing
parent4fdfc180bb2de6430537c7cff5d32b36c7bb8354 (diff)
Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fix for Rocq/Rational.)
Diffstat (limited to 'parsing')
0 files changed, 0 insertions, 0 deletions