rename
This commit is contained in:
parent
1e30753ba9
commit
84472e93dd
160 changed files with 18460 additions and 90 deletions
16
.jjconflict-side-0/tools/dune
Normal file
16
.jjconflict-side-0/tools/dune
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
(executable
|
||||
(public_name offline)
|
||||
(name offline)
|
||||
(modules offline offline_impl)
|
||||
(libraries cmdliner bos fmt mirage-crypto ptime mte vif))
|
||||
|
||||
(executable
|
||||
(public_name gen_registry_files)
|
||||
(name gen_registry_files)
|
||||
(modules gen_registry_files)
|
||||
(libraries recfile_parser bos fmt))
|
||||
|
||||
(library
|
||||
(name recfile_parser)
|
||||
(modules recfile_parser)
|
||||
(libraries angstrom bos cmdliner fmt))
|
||||
Loading…
Add table
Add a link
Reference in a new issue