+option -c

Change remote origin -> gdb.

diff --git a/bin/dashtopatch b/bin/dashtopatch
index bab4561..c48fad6 100755 (executable)
--- a/bin/dashtopatch
+++ b/bin/dashtopatch
@@ -1,25 +1,33 @@
 #! /bin/sh
 set -ex
 #! /bin/sh
 set -ex

+compile=false
+if [ "$1" = -c ];then
+  compile=true
+  shift
+fi

 if [ $# != 1 ] || ! echo "$1" | grep -q '-';then
   echo >&2 "Syntax: $0 branch-list-delimited-by-dashes"
   exit 1
 fi
 if [ $# != 1 ] || ! echo "$1" | grep -q '-';then
   echo >&2 "Syntax: $0 branch-list-delimited-by-dashes"
   exit 1
 fi

-base="origin/master"
+base="gdb/master"

 gerrit=true
 if git branch -D gerrit;then
 gerrit=true
 if git branch -D gerrit;then

-  git checkout origin/master
+  git checkout gdb/master

   git checkout -b gerrit
 else
   gerrit=false
 fi
 for elem in $(echo "$1"|tr '-' ' ');do
   git checkout -b gerrit
 else
   gerrit=false
 fi
 for elem in $(echo "$1"|tr '-' ' ');do

-  if [ "$base" = "origin/master" ];then
+  if [ "$base" = "gdb/master" ];then

     next="$elem"
   else
     next="$base-$elem"
   fi
   git checkout "$next"
   git merge "$base"
     next="$elem"
   else
     next="$base-$elem"
   fi
   git checkout "$next"
   git merge "$base"

+  if $compile;then
+    make
+  fi

   if [ -e "$next".patch ];then
     echo -e '/^--- /,$d\nw'|ed "$next".patch || :
   fi
   if [ -e "$next".patch ];then
     echo -e '/^--- /,$d\nw'|ed "$next".patch || :
   fi