diff options
| author | letouzey | 2010-03-04 16:18:21 +0000 |
|---|---|---|
| committer | letouzey | 2010-03-04 16:18:21 +0000 |
| commit | 2a0b8d89809fdfd48274359c15ba16d98df95a00 (patch) | |
| tree | 42bcca205f16e6d76e0132f610545ec2fb999bed /doc/tutorial | |
| parent | b1edecb1b38df8a88552aa4251982238b3c3125d (diff) | |
Makefile: cleanup of variables containing lists of files, such as MLFILES
- We clarify their definition via some custom make function: find, diff...
- We avoid duplications via some $(sort ...)
- Some name changes:
* old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from
.mly and .mll aren't in it anymore).
* new $(MLFILES) contains all .ml, either static or generated from
.mly .mll .ml4 or _mod.ml made out of .mllib
* $(ML4FILESML) is now $(GENML4FILES)
...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/tutorial')
0 files changed, 0 insertions, 0 deletions