Merge pull request #245 from edx/jkarni/feature/createdevfolder
Greater dir naming flexibility.
This commit is contained in:
@@ -98,19 +98,23 @@ clone_repos() {
|
||||
|
||||
set_base_default() { # if PROJECT_HOME not set
|
||||
# 2 possibilities: this is from cloned repo, or not
|
||||
# this script is in "./scripts" if a git clone
|
||||
this_repo=$(cd "${BASH_SOURCE%/*}/.." && pwd)
|
||||
if [[ "${this_repo##*/}" = "edx-platform" && -d "$this_repo/.git" ]]; then
|
||||
# set BASE one-up from this_repo;
|
||||
echo "${this_repo%/*}"
|
||||
|
||||
# See if remote's url is named edx-platform (this works for forks too, but
|
||||
# not if the name was changed).
|
||||
cd "$( dirname "${BASH_SOURCE[0]}" )"
|
||||
this_repo=$(basename $(git ls-remote --get-url 2>/dev/null) 2>/dev/null) ||
|
||||
echo -n ""
|
||||
|
||||
if [[ "x$this_repo" = "xedx-platform.git" ]]; then
|
||||
# We are in the edx repo and already have git installed. Let git do the
|
||||
# work of finding base dir:
|
||||
echo "$(dirname $(git rev-parse --show-toplevel))"
|
||||
else
|
||||
echo "$HOME/edx_all"
|
||||
fi
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
### START
|
||||
|
||||
PROG=${0##*/}
|
||||
|
||||
Reference in New Issue
Block a user