summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment3
1 files changed, 3 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
index cc22a160..b45941ab 100644
--- a/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment
+++ b/doc/todo/spin_without_remote_compilation/comment_7_3fed94d212de0e4ad2d2364cc91e6c94._comment
@@ -12,4 +12,7 @@ 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.
+
+(origin/precompiled has the above branch and has had current master
+cleanly merged into it, and builds successfully.)
"""]]