Skip to content

Commit 9b91b89

Browse files
committed
finalized create-forks-on-github.sh
1 parent 8b11d35 commit 9b91b89

2 files changed

Lines changed: 22 additions & 4 deletions

File tree

docs/replication/README.md

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,21 @@ can be removed and the actual path can be set.
2222
To execute the printed commands uncomment the last line of the second paragraph
2323
which disables `DRY_RUN`.
2424

25+
---
26+
Warning: This script doesn't properly replicate the repositories `libxml2` and
27+
`gcc`. To manually finish the replication process for these repositories, run
28+
the following in the `DiffDetectiveMining` directory (sibling of the
29+
`DiffDetective` repository manually:
30+
```
31+
for repo in libxml2 gcc
32+
do
33+
pushd "$repo"
34+
git remote add origin "[email protected]:DiffDetective/$repo.git"
35+
git push -f origin
36+
popd
37+
done
38+
```
39+
2540
## Login
2641
You can either login beforehand with `gh auth login` or just run the script
2742
which will run this command for you. This script will *not* log you out once

docs/replication/create-forks-on-github.sh

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
# Default settings
44
PATH_TO_REPOSITORIES="$(dirname "${BASH_SOURCE[0]}")/../../../DiffDetectiveMining"
5-
DRY_RUN=y
5+
DRY_RUN=n
66

77
# Override settings
88
#PATH_TO_REPOSITORIES="absolute/path/to/directory/containing/the/respositories"
@@ -16,6 +16,7 @@ continue-with() {
1616
}
1717

1818
run() {
19+
echo
1920
echo "\$ $*"
2021
if [ "$DRY_RUN" = "n" ]
2122
then
@@ -55,15 +56,17 @@ do
5556
echo
5657
run cd "$repository"
5758
url="$(git remote get-url origin)"
58-
if [[ "$url" ~= github.com ]]
59+
if [[ "$url" =~ github.com ]]
5960
then
6061
echo "$repository is a github repo"
61-
run gh repo fork --remote
62+
run gh repo fork --remote || echo "already forked"
6263
run git push -f origin
6364
else
6465
echo "$repository is not a github repo"
65-
run gh repo create "$repository" -d "Fork of $url" --push --public --source .
66+
run git remote rename origin upstream &>/dev/null
67+
run gh repo create "DiffDetective/$(basename "$repository")" -d "Fork of $url" --push --public --source .
6668
fi
69+
echo "repo succesful"
6770
done
6871

6972
if [ "$was_logged_in" = "1" ]

0 commit comments

Comments
 (0)