Skip to content

Removing CI action #35

@ybertot

Description

@ybertot

For this project, it seems that continuous integration is overkill. I am inclined to removing it. I feel like crying every time I checkpoint a part of my development and this runs CI, when I know perfectly well now is not the time to check for a complete re-compilation of the whole project.

At the very least, we should not run CI on theories when the only changes happened in the documents/ directory. I have a vague memory that we already discussed this, probably on zulip, but I am unable to find a trace of this conversation.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions