summary refs log tree commit diff
path: root/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml')
-rw-r--r--pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml19
1 files changed, 0 insertions, 19 deletions
diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml b/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml
deleted file mode 100644
index f85a7a6c5fd..00000000000
--- a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml
+++ /dev/null
@@ -1,19 +0,0 @@
-(* ------------------------------------------------------------------------- *)
-(* Create a standalone HOL image. Assumes that we are running under Linux    *)
-(* and have the program "dmtcp" available to create checkpoints.             *)
-(* ------------------------------------------------------------------------- *)
-
-let dmtcp_checkpoint, dmtcp_selfdestruct =
-  let call_dmtcp opts bannerstring =
-    let longer_banner = startup_banner ^ " with DMTCP" in
-    let complete_banner =
-      if bannerstring = "" then longer_banner
-      else longer_banner^"\n        "^bannerstring in
-    (Gc.compact(); Unix.sleep 1;
-     Format.print_string "Checkpointing..."; Format.print_newline();
-     try ignore(Unix.system ("dmtcp_command -bc " ^ opts))
-     with Unix.Unix_error _ -> ();
-     Format.print_string complete_banner;
-     Format.print_newline(); Format.print_newline())
-  in
-  call_dmtcp "", call_dmtcp "-q";;