diff options
| author | Gaëtan Gilbert | 2021-02-16 13:05:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-16 13:07:14 +0100 |
| commit | 43ed1525126723858e6e3cbd63f26dc2af479511 (patch) | |
| tree | d2e6b323d69fbed638d5a26119959903183bea85 /doc/plugin_tutorial/Makefile | |
| parent | c0e0e637c61e075f43b73d1ddd8eaa9d79b27561 (diff) | |
Only run windows job when WINDOWS=enabled
This seems to have been missed in
https://github.com/coq/coq/pull/13598
(16cd0d5cfc0c4702b8220dad8e91f31a89d904ba)
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions