Skip to content

Commit

Permalink
Merge pull request #107 from proux01/cleanup-dev-ci
Browse files Browse the repository at this point in the history
Cleanup dev/ci
  • Loading branch information
proux01 authored Feb 13, 2025
2 parents ddae606 + d51bacd commit 9ff1006
Show file tree
Hide file tree
Showing 91 changed files with 2 additions and 2,489 deletions.
4 changes: 2 additions & 2 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -679,7 +679,7 @@ documentation should be improved.

[coq-contributing-guide]: https://github.com/coq/coq/blob/master/CONTRIBUTING.md
[stdlib-repository]: https://github.com/coq-community/stdlib
[CI-README]: dev/ci/README.md
[CI-README]: dev/doc/README-CI.md
[CODEOWNERS]: .github/CODEOWNERS
[coqbot-minimize]: https://github.com/coq/coq/wiki/Coqbot-minimize-feature
[coqdoc-documentation]: https://coq.inria.fr/refman/practical-tools/utilities.html#documenting-coq-files-with-coqdoc
Expand Down Expand Up @@ -717,5 +717,5 @@ documentation should be improved.
[release-plan]: https://github.com/coq/coq/wiki/Release-Plan
[stdlib-doc]: https://coq.inria.fr/stdlib/
[test-suite-README]: test-suite/README.md
[user-overlays]: dev/ci/user-overlays
[user-overlays]: dev/doc/README-CI.md
[Zulip]: https://coq.zulipchat.com/#narrow/channel/478198-Stdlib-devs-.26-users
2 changes: 0 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -21,5 +21,3 @@ refman-html:

stdlib-html:
$(DUNE) build --root . @stdlib-html

include Makefile.ci
206 changes: 0 additions & 206 deletions Makefile.ci

This file was deleted.

15 changes: 0 additions & 15 deletions dev/ci/ci-aac_tactics.sh

This file was deleted.

15 changes: 0 additions & 15 deletions dev/ci/ci-analysis.sh

This file was deleted.

15 changes: 0 additions & 15 deletions dev/ci/ci-argosy.sh

This file was deleted.

15 changes: 0 additions & 15 deletions dev/ci/ci-async_test.sh

This file was deleted.

15 changes: 0 additions & 15 deletions dev/ci/ci-atbr.sh

This file was deleted.

15 changes: 0 additions & 15 deletions dev/ci/ci-autosubst.sh

This file was deleted.

16 changes: 0 additions & 16 deletions dev/ci/ci-autosubst_ocaml.sh

This file was deleted.

Loading

0 comments on commit 9ff1006

Please sign in to comment.