diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-13 19:33:44 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-13 19:33:53 +0200 |
| commit | 25462addaf604ff51e886bbc92937bb272982b04 (patch) | |
| tree | c0b30236ab923fbcea25a4cdcd2f09e011817418 /theories | |
| parent | 91c67be4732a5281df9007cf505af251de62b9ea (diff) | |
Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709)
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions