1 files changed, 16 insertions, 0 deletions
diff --git a/src/boot/driver/glue.ml b/src/boot/driver/glue.ml
new file mode 100644
index 00000000..4fc74480
--- /dev/null
+++ b/src/boot/driver/glue.ml
@@ -0,0 +1,16 @@
+(*
+ * Glue, or lack thereof, for the standard x86 backend.
+ *)
+
+let alt_argspecs _ = [];;
+let alt_pipeline _ _ _ = ();;
+
+(*
+ * Local Variables:
+ * fill-column: 78;
+ * indent-tabs-mode: nil
+ * buffer-file-coding-system: utf-8-unix
+ * compile-command: "make -k -C ../.. 2>&1 | sed -e 's/\\/x\\//x:\\//g'";
+ * End:
+ *)
+