The username under which gitlab is running, has changed from gitlab to git. If you get the following message when pushing or pulling: Permission denied (publickey), then execute this command in your repository directory: git remote set-url origin . (replace namespace and project by the appropriate values). Use git remote -v to check the current value.

Commit 87d971a4 authored by remivantrijp's avatar remivantrijp

Minor correction.

parent dd6b1628
......@@ -40,7 +40,8 @@
;; ---------------------------------------------------------------
(clause ()
(referent ?ref)
(syn-cat ((is-matrix-clause ?plus-or-minus))))
(syn-cat ((is-matrix-clause ?plus-or-minus)
(clause-type ?clause-type))))
(matrix-clause (clause)
(syn-cat ((is-matrix-clause +))))
(subclause (clause)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment