Commit Graph

16 Commits

Author SHA1 Message Date
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