Closed F1nnM closed 3 years ago
Swapped the parameters 'Rightarrow' and 'no head' in diagram.js
Interesting, this indeed solves the problem, thanks!
Swapped the parameters 'Rightarrow' and 'no head' in diagram.js