From d9dd266345eda045873f8bf037eac7a984a8a65f Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Thu, 9 Nov 2017 15:49:38 +1100
Subject: [PATCH] Support custom poly-includes.ML for worker

---
 worker.sml | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/worker.sml b/worker.sml
index c397db8..b3e289d 100644
--- a/worker.sml
+++ b/worker.sml
@@ -173,6 +173,18 @@ end
 fun ensure_hol_exists () = ensure_clone_exists hol_remote "--single-branch " HOLDIR
 fun ensure_cakeml_exists () = ensure_clone_exists cakeml_remote "" CAKEMLDIR
 
+fun link_poly_includes () =
+  let
+    val includes_file = "poly-includes.ML"
+    val f = OS.Path.concat(OS.Path.parentArc,includes_file)
+  in
+    if OS.FileSys.access(f,[OS.FileSys.A_READ]) then
+      Posix.FileSys.symlink { old = OS.Path.concat(OS.Path.parentArc,f),
+                              new = OS.Path.concat("tools-poly",includes_file) }
+      before diag ["linking to custom ",includes_file]
+    else ()
+  end
+
 fun prepare_hol sha =
   let
     val () = ensure_hol_exists ()
@@ -184,7 +196,8 @@ fun prepare_hol sha =
       if reuse
       then diag ["re-using HOL working directory at same commit"]
       else (system_output (git_reset sha);
-            ignore (system_output git_clean))
+            system_output git_clean;
+            link_poly_includes ())
     val () = OS.FileSys.chDir OS.Path.parentArc
   in
     reuse