diff options
1 files changed, 15 insertions, 0 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
new file mode 100644
index 00000000..8046810c
--- /dev/null
+++ b/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment
@@ -0,0 +1,15 @@
+[[!comment format=mdwn
+ username="joey"
+ subject="""comment 7"""
+ date="2017-12-03T18:20:25Z"
+ content="""
+Felix did some more work on this last April, in his precompiled-rebased
+In particular, that branch is supposed to handle case #3 above (by a git
+clone to temp dir and move of the files).
+Felix said he had not tested it, and I have not tested it either. If
+someone can try his branch and confirm that it works, including handling
+of cases #2 and #3 above, I'd be happy to merge it.