diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-12 18:17:17 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-07-12 18:22:07 +0200 |
| commit | 605048905db9107a1d4b3c35ce59f5719474f875 (patch) | |
| tree | a9d70ba8fe15f04b1e2ae2a3e9117f8a263c8ba9 /interp/ppextend.ml | |
| parent | ea25e8bcf64caac66bcbd33457ee91d56e80fea3 (diff) | |
Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4
- With the ?= construction, we avoid warnings about undefined variables,
while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make'
- Some extra documentation and cleanup
Diffstat (limited to 'interp/ppextend.ml')
0 files changed, 0 insertions, 0 deletions