diff options
| author | Daniel Mendler <mail@daniel-mendler.de> | 2023-02-01 10:44:31 +0100 |
|---|---|---|
| committer | Daniel Mendler <mail@daniel-mendler.de> | 2023-02-01 10:44:31 +0100 |
| commit | d85e90bf1f917aae11367eb62d35d2c423c6173c (patch) | |
| tree | 19561987b163bc95097594734ecdddd941d60ff0 /.github/workflows | |
| parent | b1e2a804a453ee93713a5a4ad8c45a134dffbcb8 (diff) | |
CI: Do not ignore texi
We test in CI if the manuals builds.
Diffstat (limited to '.github/workflows')
| -rw-r--r-- | .github/workflows/makefile.yml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/.github/workflows/makefile.yml b/.github/workflows/makefile.yml index 0764e34..f0ae185 100644 --- a/.github/workflows/makefile.yml +++ b/.github/workflows/makefile.yml @@ -5,12 +5,10 @@ on: paths-ignore: - '**.md' - '**.org' - - '**.texi' pull_request: paths-ignore: - '**.md' - '**.org' - - '**.texi' jobs: test: |