diff options
Diffstat (limited to 'src/GNUmakefile')
| -rw-r--r-- | src/GNUmakefile | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/GNUmakefile b/src/GNUmakefile index ab35c7e..f61ae63 100644 --- a/src/GNUmakefile +++ b/src/GNUmakefile @@ -144,6 +144,15 @@ endif ifdef DUMP_TREE PROFILE += -DDUMP_TREE endif +ifdef CALIBRATE_POSITIONAL +PROFILE += -DCALIBRATE_POSITIONAL +endif +ifdef CALIBRATE_BASE_MARGIN +PROFILE += -DCALIBRATE_BASE_MARGIN +endif +ifdef CALIBRATE_MARGIN_SAFETY +PROFILE += -DCALIBRATE_MARGIN_SAFETY +endif endif # EVERYTHING # Short commit hash (plus a -dirty suffix if the working tree has |