diff options
| author |  Jason Gross <jgross@mit.edu> | 2014-01-16 17:29:39 -0500 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-01-18 11:56:30 +0100 |
| commit | 22bd27a46f6c91f2c74945333547e4657dcd1428 (patch) | |
| tree | 3676981d9ec69f0e1e18c361181d33bad3550365 /checker/inductive.ml | |
| parent | 151508e04e56e1d090b22101b277803ec5d45815 (diff) | |
Makefiles use $(foo), not $foo, for variables
Also, we need :=, so that it's evaluated immediately, rather than
becoming a self-recursive variable. This fixes the "Undefined variable
'C'" error that make keeps spewing.
Diffstat (limited to 'checker/inductive.ml')
0 files changed, 0 insertions, 0 deletions