15 Commits

Include renames

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