Announcement: Git conversion



> < I see. Then I recommend that we remove izic, CVSROOT and htdocs from
> < the repository. Maybe also maxima-pre59 and maximabook since these are
> < also not used anymore.
>  
>  Well, the virtue and curse of a repository is that nothing is ever
>  really deleted from it (btw, htdocs stores all our webpage stuff.)
> 
>  If you don't like having these directories in your working copy, then what
>  you can do is
> 
>  git update-index --assume-unchanged [directories] #and maybe files
>  rm -fr [directories]
> 
>  This removes those files from your working copy and ensures that Git
>  doesn't try to update them. It does not remove them from your
>  repository.
>

I guess it's clear but just to mention: Of course one can removes files
from a repository, I recommend "git rm file(s)-or-directories", but it
stays in the history. Normally this is a good thing, and I don't think
that space should be a big isue here. However, if really needed, then one can
do "history-surgery", and really remove something (but this should only be done
in this initial phase, before the repositories go public).

Oliver