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 42c0cd6a authored by remivantrijp's avatar remivantrijp


parent 0ee77487
......@@ -158,6 +158,7 @@
(append conjunctors units-to-append))))
;; (comprehend "I like Mickey Mouse and Donald Duck.")
;; (comprehend "Do you prefer Mickey Mouse, Donald Duck or Goofy?")
;;;;; ----------------------------------------------------------------------------------------------------------------------
;;;;; CLAUSAL units
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