summaryrefslogtreecommitdiff
path: root/config
diff options
context:
space:
mode:
Diffstat (limited to 'config')
-rw-r--r--config/global/paths.in22
1 files changed, 22 insertions, 0 deletions
diff --git a/config/global/paths.in b/config/global/paths.in
index 341d207..b97e258 100644
--- a/config/global/paths.in
+++ b/config/global/paths.in
@@ -61,6 +61,28 @@ config INSTALL_DIR
# The reason you might also want to install elsewhere is if you are going
# to package your shinny new toolchain for distribution.
+config RM_RF_PREFIX_DIR
+ bool
+ prompt "| Remove the prefix dir prior to building"
+ default y
+ depends on !BACKEND
+ help
+ If you say 'y' here, then PREFIX_DIR (above) will be eradicated
+ prior to the toolchain is built.
+
+ This can be usefull when you are trying different settings (due
+ to build failures or feature tests). In this case, to avoid using
+ a potentially broken previous toolchain, the install location is
+ removed, to start afresh.
+
+ On the oher hand, if you are building a final toolchain, and install
+ it into a directory with pre-install, unrelated programs, it would be
+ damageable to remove that directory. In this case, you may want to
+ say 'n' here.
+
+ Note that when acting as a backend, this option is not available, and
+ is forced to 'n'.
+
config REMOVE_DOCS
bool
prompt "Remove documentation"