]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ac91e70) | patch
Makefiles removed in favour of dune-only solution
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 3 Jan 2023 16:27:07 +0000 (17:27 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Feb 2023 14:23:41 +0000 (15:23 +0100)
commita19551fd50df93951d78eea4c163d434f844047c
treed94627a6605f650e0d38125641d905c4c28cc194tree | snapshot
parentac91e70f52b1e56fa6729399026c06722f4a7e8bcommit | diff
Makefiles removed in favour of dune-only solution

- some Makefiles are still to be removed
- some Makefiles in legacy dirs that are no longer compiled will
  be kept
- the Makefile in help is still useful!
28 files changed:
matita/components/content/Makefile [deleted file] blob | history
matita/components/content_pres/Makefile [deleted file] blob | history
matita/components/disambiguation/Makefile [deleted file] blob | history
matita/components/disambiguation/disambiguate.crit2.ml [deleted file] blob | history
matita/components/disambiguation/disambiguate.crit2_ml [new file with mode: 0644] blob
matita/components/disambiguation/disambiguate.crit4.ml [deleted file] blob | history
matita/components/disambiguation/disambiguate.crit4_ml [new file with mode: 0644] blob
matita/components/extlib/Makefile [deleted file] blob | history
matita/components/getter/Makefile [deleted file] blob | history
matita/components/grafite/Makefile [deleted file] blob | history
matita/components/grafite_engine/Makefile [deleted file] blob | history
matita/components/grafite_parser/Makefile [deleted file] blob | history
matita/components/library/Makefile [deleted file] blob | history
matita/components/logger/Makefile [deleted file] blob | history
matita/components/ng_cic_content/Makefile [deleted file] blob | history
matita/components/ng_disambiguation/Makefile [deleted file] blob | history
matita/components/ng_extraction/Makefile [deleted file] blob | history
matita/components/ng_kernel/Makefile [deleted file] blob | history
matita/components/ng_library/Makefile [deleted file] blob | history
matita/components/ng_paramodulation/Makefile [deleted file] blob | history
matita/components/ng_refiner/Makefile [deleted file] blob | history
matita/components/ng_tactics/Makefile [deleted file] blob | history
matita/components/registry/Makefile [deleted file] blob | history
matita/components/syntax_extensions/Makefile [deleted file] blob | history
matita/components/syntax_extensions/dune diff | blob | history
matita/components/thread/Makefile [deleted file] blob | history
matita/components/xml/Makefile [deleted file] blob | history
matita/matita/help/C/Makefile diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.