diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-04 16:18:09 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-04 16:18:09 +0000 |
| commit | 139bf11029dc16bf95c56646c41457b14cc35fdc (patch) | |
| tree | a3033255a7780e7a6d83408adc16a3084c9b5a9f /dev | |
| parent | 58a5a535b138c6a3e98bc3631ebe3e0e2bc3fcd5 (diff) | |
Makefile: factorization of default rules for .cmi/.cmo/.cmx
We use some conditional variables $(if ...) to set the proper flags
instead of fully duplicating the rules according to the path
checker/%.cm? ide/%.cm? %.cm?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12834 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions