Commit Graph

22 Commits

Author SHA1 Message Date
Nicolas Saillant 349ad3cf14 Add workflow_dispatch 2023-01-18 11:52:47 +01:00
Sébastien Loriot 2394f79090 update command 2022-07-18 14:54:51 +02:00
dependabot[bot] 89898a5f92
Bump actions/checkout from 2 to 3
Bumps [actions/checkout](https://github.com/actions/checkout) from 2 to 3.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](https://github.com/actions/checkout/compare/v2...v3)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
2022-06-24 07:10:25 +00:00
naveen 03023aa08f chore: Set permissions for GitHub actions
Restrict the GitHub token permissions only to the required ones; this way, even if the attackers will succeed in compromising your workflow, they won’t be able to do much.

- Included permissions for the action. https://github.com/ossf/scorecard/blob/main/docs/checks.md#token-permissions

https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#permissions

https://docs.github.com/en/actions/using-jobs/assigning-permissions-to-jobs

[Keeping your GitHub Actions and workflows secure Part 1: Preventing pwn requests](https://securitylab.github.com/research/github-actions-preventing-pwn-requests/)

Signed-off-by: naveen <172697+naveensrinivasan@users.noreply.github.com>
2022-06-23 00:31:13 +00:00
Sébastien Loriot 0f90757b21 Merge remote-tracking branch 'cgal/5.3.x-branch' 2022-05-13 17:25:21 +02:00
Sébastien Loriot b4d06c6fd1 remove Maxime from scripts 2022-05-06 14:04:25 +02:00
Laurent Rineau da9baf7e08 Fix a bug in the workflow "Documentation Removal" 2021-09-29 11:59:27 +02:00
Maxime Gimeno 9e29edb42c Fix condition for push 2021-07-07 15:10:09 +02:00
Maxime Gimeno 7161686c46 fix !git into ! git 2021-02-09 15:00:33 +01:00
Maxime Gimeno 02708a3e6a Fix delete_doc 2020-10-28 13:50:58 +01:00
Maxime Gimeno 5765a203ff Fix auto doc scripts 2020-10-28 11:08:24 +01:00
Maxime Gimeno 902284e45d Same for doc removal 2020-10-26 15:27:09 +01:00
Maxime Gimeno 3319fdf8e9 WIP filtering 2020-10-23 15:28:17 +02:00
Maxime Gimeno 3289e577fa test if index changed before pushing. 2020-09-28 07:24:14 +02:00
Maxime Gimeno 806399c3c7 Use egrep and github token 2020-09-22 14:51:01 +02:00
Maxime Gimeno 89c135aff7 Only remove the PR name in the index, not in the repo. 2020-09-10 14:31:22 +02:00
Maxime Gimeno 94f1c7cbe9 update index too 2020-09-09 12:48:56 +02:00
Maxime Gimeno 1f11e5d861 Don't use gf.com but only git 2020-09-09 11:18:51 +02:00
Maxime Gimeno de24c4729a Clena-up 2020-09-09 11:18:51 +02:00
Maxime Gimeno 08600afd72 Add a github manip 2020-09-09 11:18:51 +02:00
Maxime Gimeno 9cae0bdad7 Remove dir on pr closed 2020-09-09 11:18:51 +02:00
Maxime Gimeno d8bd7c90d7 delete PR on delete 2020-09-09 11:18:51 +02:00