1
0
Fork 0

change branch form dev to master

This commit is contained in:
Kim, Jimin 2022-01-28 11:15:50 +09:00
parent d1315780ce
commit 7edc63ca83

View file

@ -64,9 +64,8 @@ def minimal_initialization():
if os.path.exists(tmp_dir):
rmtree(tmp_dir)
# todo: change branch to master when merging with master
if os.system(
f"git clone --depth 1 -b dev https://github.com/developomp/setup.git {tmp_dir} &> /dev/null"
f"git clone --depth 1 https://github.com/developomp/setup.git {tmp_dir} &> /dev/null"
):
print("Failed to clone repository", file=sys.stderr)
exit(1)