diff options
Diffstat (limited to 'Makefile.config.in')
| -rw-r--r-- | Makefile.config.in | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 35f7bcfe..a6dcdcaa 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -29,6 +29,12 @@ PROJ_INSTALL_ROOT := @prefix@ STP_ROOT := @STP_ROOT@ +STP_NEEDS_BOOST := @STP_NEEDS_BOOST@ + +ifeq ($(STP_NEEDS_BOOST),1) + UPSTREAM_STP_LINK_FLAGS = @UPSTREAM_STP_LINK_FLAGS@ +endif + ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ |