Skip to content

Commit d964423

Browse files
committed
Provide an interface for driver/optmain.ml
1 parent a162163 commit d964423

File tree

2 files changed

+24
-2
lines changed

2 files changed

+24
-2
lines changed

.depend

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6162,9 +6162,12 @@ driver/opterrors.cmx : \
61626162
driver/opterrors.cmi
61636163
driver/opterrors.cmi :
61646164
driver/optmain.cmo : \
6165-
driver/optmaindriver.cmi
6165+
driver/optmaindriver.cmi \
6166+
driver/optmain.cmi
61666167
driver/optmain.cmx : \
6167-
driver/optmaindriver.cmx
6168+
driver/optmaindriver.cmx \
6169+
driver/optmain.cmi
6170+
driver/optmain.cmi :
61686171
driver/optmaindriver.cmo : \
61696172
utils/warnings.cmi \
61706173
utils/profile.cmi \

driver/optmain.mli

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
(**************************************************************************)
2+
(* *)
3+
(* OCaml *)
4+
(* *)
5+
(* Sebastien Hinderer, projet Cambium, INRIA Paris *)
6+
(* *)
7+
(* Copyright 2022 Institut National de Recherche en Informatique et *)
8+
(* en Automatique. *)
9+
(* *)
10+
(* All rights reserved. This file is distributed under the terms of *)
11+
(* the GNU Lesser General Public License version 2.1, with the *)
12+
(* special exception on linking described in the file LICENSE. *)
13+
(* *)
14+
(**************************************************************************)
15+
16+
(* Interface to the native compiler's main module *)
17+
18+
(* This interface file is empty because driver/optmain.ml only runs
19+
code during initialisation and exports nothing *)

0 commit comments

Comments
 (0)