diff options
| author | lmamane | 2007-01-17 18:01:02 +0000 |
|---|---|---|
| committer | lmamane | 2007-01-17 18:01:02 +0000 |
| commit | b6e48edfe3a3df123ea8e3de81d96866ae54d553 (patch) | |
| tree | f5e46b9eb70027daa2b99a4fa9f3b51a365cfd0f /dev/include | |
| parent | 8361c31cd14e95ae34386685e94a7fea86563d14 (diff) | |
Reintroduce compatibility with old versions of GNU make
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9497 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions