Skip to content

Commit 9ff1006

Browse files
authored
Merge pull request #107 from proux01/cleanup-dev-ci
Cleanup dev/ci
2 parents ddae606 + d51bacd commit 9ff1006

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

91 files changed

+2
-2489
lines changed

CONTRIBUTING.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -679,7 +679,7 @@ documentation should be improved.
679679

680680
[coq-contributing-guide]: https://github.com/coq/coq/blob/master/CONTRIBUTING.md
681681
[stdlib-repository]: https://github.com/coq-community/stdlib
682-
[CI-README]: dev/ci/README.md
682+
[CI-README]: dev/doc/README-CI.md
683683
[CODEOWNERS]: .github/CODEOWNERS
684684
[coqbot-minimize]: https://github.com/coq/coq/wiki/Coqbot-minimize-feature
685685
[coqdoc-documentation]: https://coq.inria.fr/refman/practical-tools/utilities.html#documenting-coq-files-with-coqdoc
@@ -717,5 +717,5 @@ documentation should be improved.
717717
[release-plan]: https://github.com/coq/coq/wiki/Release-Plan
718718
[stdlib-doc]: https://coq.inria.fr/stdlib/
719719
[test-suite-README]: test-suite/README.md
720-
[user-overlays]: dev/ci/user-overlays
720+
[user-overlays]: dev/doc/README-CI.md
721721
[Zulip]: https://coq.zulipchat.com/#narrow/channel/478198-Stdlib-devs-.26-users

Makefile

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,5 +21,3 @@ refman-html:
2121

2222
stdlib-html:
2323
$(DUNE) build --root . @stdlib-html
24-
25-
include Makefile.ci

Makefile.ci

Lines changed: 0 additions & 206 deletions
This file was deleted.

dev/ci/ci-aac_tactics.sh

Lines changed: 0 additions & 15 deletions
This file was deleted.

dev/ci/ci-analysis.sh

Lines changed: 0 additions & 15 deletions
This file was deleted.

dev/ci/ci-argosy.sh

Lines changed: 0 additions & 15 deletions
This file was deleted.

dev/ci/ci-async_test.sh

Lines changed: 0 additions & 15 deletions
This file was deleted.

dev/ci/ci-atbr.sh

Lines changed: 0 additions & 15 deletions
This file was deleted.

dev/ci/ci-autosubst.sh

Lines changed: 0 additions & 15 deletions
This file was deleted.

dev/ci/ci-autosubst_ocaml.sh

Lines changed: 0 additions & 16 deletions
This file was deleted.

0 commit comments

Comments
 (0)