diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-18 21:04:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-18 21:04:22 +0100 |
| commit | ce22501ca90e3c6e7124de4eeb4ad3c0a2615666 (patch) | |
| tree | 106ff9673f79dcb2b034b62af1a39b6317b1f113 /lib/unionfind.ml | |
| parent | 80158e796b6df8eb36117f349c312127c5729a8c (diff) | |
Gitlab: don't ./configure in documentation job
The config/Makefile is carried over by artefacts.
Diffstat (limited to 'lib/unionfind.ml')
0 files changed, 0 insertions, 0 deletions