Skip to content

Remove "QUIT" from makedoc.g #112

@fingolfin

Description

@fingolfin

I am tempted to remove the "QUIT" from the end of our makedoc.g.

Thing is, the only thing it does is to make gap makedoc.g a convenient command. But gap < makedoc.g is similarly convenient, and many projects also allow make doc.

On the other hand, it makes it impossible to use makedoc.g from other GAP scripts without spawning a fresh GAP interpreter. This is why my release tools ends up starting 4 or 5 GAP processes -- if makedoc.g did not QUIT (and also update.g from GitHubPageForGAP), I think I could get this down to one or two.

But perhaps I am missing reasons why the QUIT really is a good idea... Thoughts?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions