Commit 1e27583
committed
Remove GitHub Workflow for mirroring to Gitlab
There was an advent recently, the Pipelines in Gitlab took a very long
time to execute, and used up my entire quota of free runners. At first
I thought of just adding timeouts, but then I thought there might be
better approaches to integrating with Gitlab.
So I'm removing the Gitlab integration for now, maybe in the future
when quotas are restored I'll set up a more convenient and thoughtful
integration again.1 parent 1023c34 commit 1e27583
2 files changed
+0
-25
lines changedThis file was deleted.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
2 | 2 | | |
3 | 3 | | |
4 | 4 | | |
5 | | - | |
6 | | - | |
7 | 5 | | |
8 | 6 | | |
9 | 7 | | |
| |||
0 commit comments