]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f47c4a4) | patch
Fix "dune build" for syntax_extensions
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 2 Jan 2023 19:56:40 +0000 (20:56 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 2 Jan 2023 19:56:40 +0000 (20:56 +0100)
commit413ab5643bc3c204edd97e348bb0cbff9c77d2c9
tree8dbf2ef72fd45805623fa8d6fcc2b78ecc3d3844tree | snapshot
parentf47c4a4cc2f6483ea7a333844f90c14039f99d1acommit | diff
Fix "dune build" for syntax_extensions

- pa_unicode_macro.cma no longer "includes" helm_syntax_extensions.cma

The only reason for this change, that makes camlp5o harder to call, is
that dune enforces modules to belong to one library only.
matita/components/content_pres/dune diff | blob | history
matita/components/grafite_parser/dune diff | blob | history
matita/components/syntax_extensions/dune diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.