diff options
author | david <david@web> | 2020-05-16 23:12:20 +0000 |
---|---|---|
committer | admin <admin@branchable.com> | 2020-05-16 23:12:20 +0000 |
commit | 8bc8e2d2040227af6a180466ac85bc772fb96131 (patch) | |
tree | b1da8525859e49f489d0f43d6d2e2982fef6e3ab | |
parent | 6291c48a23401647ca6ee71a307627d370d3f6c5 (diff) |
-rw-r--r-- | doc/todo/Support_for_mirroring_bare_git_repos.mdwn | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/todo/Support_for_mirroring_bare_git_repos.mdwn b/doc/todo/Support_for_mirroring_bare_git_repos.mdwn new file mode 100644 index 00000000..3c5da097 --- /dev/null +++ b/doc/todo/Support_for_mirroring_bare_git_repos.mdwn @@ -0,0 +1,2 @@ +Since "git pull" has the potential to fail because of merge problems (this is not theoretical, it happened to me today), I'd prefer to just fetch into a bare repo. +I don't know the best way to go about this. Maybe a "Git.fetched" function that does not assume a non-bare repo (as Git.cloned currently does). |