diff options
Diffstat (limited to 'package')
| -rw-r--r-- | package/xenomai/Config.in | 6 | ||||
| -rw-r--r-- | package/xenomai/xenomai.mk | 2 |
2 files changed, 8 insertions, 0 deletions
diff --git a/package/xenomai/Config.in b/package/xenomai/Config.in index 6646ec08ea..4bbffb2c21 100644 --- a/package/xenomai/Config.in +++ b/package/xenomai/Config.in @@ -120,6 +120,12 @@ config BR2_PACKAGE_XENOMAI_ENABLE_REGISTRY_PATH To use the Xenomai default (currently: /var/run/xenomai), leave this option empty. +config BR2_PACKAGE_XENOMAI_ADDITIONAL_CONF_OPTS + string "Additional configure options" + help + Specify any additional options to pass to the configure + script here. See Xenomai documentation for details. + config BR2_PACKAGE_XENOMAI_TESTSUITE bool "Install testsuite" help diff --git a/package/xenomai/xenomai.mk b/package/xenomai/xenomai.mk index 89b022a5ac..2d92e91d41 100644 --- a/package/xenomai/xenomai.mk +++ b/package/xenomai/xenomai.mk @@ -57,6 +57,8 @@ else XENOMAI_CONF_OPTS += --disable-registry endif +XENOMAI_CONF_OPTS += $(call qstrip,$(BR2_PACKAGE_XENOMAI_ADDITIONAL_CONF_OPTS)) + # Some of these files may be desired by some users -- at that point specific # config options need to be added to keep a particular set. define XENOMAI_REMOVE_UNNEEDED_FILES |
