diff options
| author | Ian Jackson <ijackson@chiark.greenend.org.uk> | 2017-08-02 19:19:38 +0100 |
|---|---|---|
| committer | Ian Jackson <ijackson@chiark.greenend.org.uk> | 2017-08-03 20:37:19 +0100 |
| commit | 8a6027965b4f02552cf754f9ec081e35c7174146 (patch) | |
| tree | 375ff6e62f8f18f6cf7021958d54c71bb67f721d /debian | |
| parent | 37923577e345babd9e21382449147053ed063f44 (diff) | |
worktree support: Fix playtree_setup
In a worktree, .git is not a directory. We need to use
$maindir_common. Add a comment, too.
Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
Diffstat (limited to 'debian')
0 files changed, 0 insertions, 0 deletions