diff options
Diffstat (limited to 'build/mixed-boot.sh')
| -rwxr-xr-x | build/mixed-boot.sh | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/build/mixed-boot.sh b/build/mixed-boot.sh deleted file mode 100755 index 057b523332..0000000000 --- a/build/mixed-boot.sh +++ /dev/null @@ -1,21 +0,0 @@ -#!/bin/sh - -######################################################################### -# # -# OCaml # -# # -# Nicolas Pouillard, projet Gallium, INRIA Rocquencourt # -# # -# Copyright 2007 Institut National de Recherche en Informatique et # -# en Automatique. All rights reserved. This file is distributed # -# under the terms of the Q Public License version 1.0. # -# # -######################################################################### - -set -ex -cd `dirname $0`/.. -touch build/ocamlbuild_mixed_mode -mkdir -p _build -cp -rf boot _build/ -./build/mk_shell_and_ocamlbuild_config.sh -./build/boot.sh |