Skip to content

add \nodetitle command to specify titles of nodes in dependency graph - #74

Open
Hagb wants to merge 1 commit into
PatrickMassot:masterfrom
WuProver:master
Open

add \nodetitle command to specify titles of nodes in dependency graph#74
Hagb wants to merge 1 commit into
PatrickMassot:masterfrom
WuProver:master

add `\nodetitle` command to specify titles of nodes in dependency graph

97a489c
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs