]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 712af5b) | 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>
Tue, 14 Feb 2023 14:23:41 +0000 (15:23 +0100)
commit596e5b93aa6733e4bcd3022da81bb5500d1a5dee
treea3eff60b11948c196bc70fa28570f0d0b047dbectree | snapshot
parent712af5b8dc7dab1ebfa6532b73b91c96cb4c6837commit | 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.