]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1f2917b) | 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, 3 Jan 2023 16:27:07 +0000 (17:27 +0100)
commitae88c7c1481ac9ddf5d55e2144b6db418a25fdd1
treec7fbdf56a987cc7147a3e5d0d890b499baf4dfbctree | snapshot
parent1f2917bc135300b4fd23314a21946e7df7933f81commit | 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.