diff options
| author | Pierre Letouzey | 2016-06-02 05:01:35 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-07 16:16:46 +0200 |
| commit | e9c57a3b6035278b0d4112da8c350a9cdd356259 (patch) | |
| tree | 174f752349d595dfa2c708858da1b283dabeea14 /plugins/syntax/string_syntax_plugin.mllib | |
| parent | af6b36dd24651f1324e7babb982a345fde7d4b58 (diff) | |
coq_makefile : short display of commands executed by make
This purely cosmetic effect is obtained by the same variables
$(SHOW) and $(HIDE) as in the main Makefile of Coq.
If you prefer the earlier raw output : make VERBOSE=1
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mllib')
0 files changed, 0 insertions, 0 deletions