diff options
| author | Gaëtan Gilbert | 2018-05-11 22:26:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-11 22:26:04 +0200 |
| commit | c24fcbe937bcb84d7fd5e441ff6cbbad589fa096 (patch) | |
| tree | b364bc04f7cbdbcd1b88aecfe3532b9b0f4a721a /dev/tools/objects.el | |
| parent | 7a6cac1942281fbd66c0e46e3be068b9198addce (diff) | |
gitlab CI: remove math-classes job
It's redundant as a dependency of formal-topology.
Diffstat (limited to 'dev/tools/objects.el')
0 files changed, 0 insertions, 0 deletions