diff options
Diffstat (limited to 'doc/todo')
| -rw-r--r-- | doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment b/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment index 8046810c..cc22a160 100644 --- a/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment +++ b/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment @@ -3,7 +3,7 @@ subject="""comment 7""" date="2017-12-03T18:20:25Z" content=""" -Felix did some more work on this last April, in his precompiled-rebased +Felix did some more work on this last April, in his precompiled-rebased-2 branch. In particular, that branch is supposed to handle case #3 above (by a git |