1 Jul
2019
1 Jul
'19
3:01 p.m.
Richard Eisenberg
Just to pass on something that looks cool (I haven't tried it myself yet): git worktree. It seems git can hang several different checkouts of a repo in different directories. This seems far superior to my current habit of having many clones of ghc, sometimes going through machinations to get commits from one place to another. The documentation for git worktree seems quite approachable, so you might find it useful. I plan on using it in the future.
Indeed I use `git new-workdir`, which is a script similar to `git worktree` (but I think predates `worktree` by a few years). Like `worktree`, this allows you to have several working directories sharing a set of refs. Cheers, - Ben