StanHeaders: Use develop branch of Stan

stan-dev · Sep 10, 2023 · be4a2c2 · be4a2c2
1 parent 951683d
commit be4a2c2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/sh_b.sh b/sh_b.sh
@@ -3,7 +3,7 @@
 red='\033[0;31m'
 NC='\033[0m' # no color
 
-STAN_REPO_BRANCH=StanHeaders_2.26
+STAN_REPO_BRANCH=develop
 grepstanbranch=`git ls-remote --heads https://github.com/stan-dev/stan.git | grep "/${STAN_REPO_BRANCH}"`
 if [ -z "$grepstanbranch" ]; then
     echo -e "${red}ERROR:${NC} stan repo does not have {STAN_REPO_BRANCH}"