summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--include/get.sh3
-rw-r--r--include/tree.sh7
2 files changed, 8 insertions, 2 deletions
diff --git a/include/get.sh b/include/get.sh
index 6c7ddcf3..1080412e 100644
--- a/include/get.sh
+++ b/include/get.sh
@@ -232,7 +232,8 @@ try_git()
x_ mv "$tmpgitcache" "$gitdest"
fi
- if git -C "$gitdest" whatchanged "$7" 1>/dev/null 2>/dev/null; then
+ if git -C "$gitdest" whatchanged "$7" 1>/dev/null 2>/dev/null && \
+ [ "$forcepull" != "y" ]; then
# don't try to pull the latest changes if the given target
# revision already exists locally. this saves a lot of time
# during release builds, and reduces the chance that we will
diff --git a/include/tree.sh b/include/tree.sh
index c0802bfe..bfb60eea 100644
--- a/include/tree.sh
+++ b/include/tree.sh
@@ -8,7 +8,7 @@ eval "`setvars "" xarch srcdir premake gnatdir xlang mode makeargs elfdir cmd \
project target target_dir targets xtree _f release bootstrapargs mkhelper \
autoconfargs listfile autogenargs btype rev build_depend gccdir cmakedir \
defconfig postmake mkhelpercfg dry dest_dir mdir cleanargs gccver gccfull \
- gnatver gnatfull do_make badhash badtghash tree`"
+ gnatver gnatfull do_make badhash badtghash tree forcepull`"
trees()
{
@@ -44,6 +44,11 @@ trees()
do_make="n" # lets us know not to build anything
dry=":"
;;
+ -F) # same as -F, but don't skip git fetch/pull on cache
+ do_make="n" # lets us know not to build anything
+ dry=":"
+ forcepull="y"
+ ;;
-s) mode="savedefconfig" ;;
-l) mode="olddefconfig" ;;
-n) mode="nconfig" ;;