I’ve created a GIT repository for cduce and few experiments of mine at http://git.cduce.org . I’m using gitweb, that is a neat piece of sw. Easy to install and to manage. I had a minor problem related to the fact I’m using http as transport protocol to clone our git repos. In particular, the error was:
$git clone http://git.cduce.org/r/hashconsing.git
Cannot get remote repository information.
Perhaps git-update-server-info needs to be run there?
The easy fix was to do what I was told to do and to run
git-update-server-info in the remote repo.
From the manpage:
A dumb server that does not do on-the-fly pack generations must have some auxiliary information files in $GIT_DIR/info and $GIT_OBJECT_DIRECTORY/info directories to help clients discover what references and packs the server has. This command generates such auxiliary files.