User

Clément Démoulins

From LRDE

Extraire des sous dossiers d'un dépôt git

Exemple, on veut extraire les papiers de Vaucanson du dépôt commun lrde-publis.

# Clone du dépôt
git clone git@git:lrde-publis.git
git clone --no-hardlinks lrde-publis vcsn-publis
cd vcsn-publis

# Filtre tout sauf ce qui match la pattern : (\.fsmnlp|\.ciaa|\.poosc|\.vaucanson|\.gitignore|\.gitmodules)$
git filter-branch --prune-empty --index-filter "git rm -r --cached --ignore-unmatch $(git log -p | sed -rne 's/^diff --git a\/([^/]+)\/?.* b\/.*$/\1/ p' | sort -u | egrep -v '(\.fsmnlp|\.ciaa|\.poosc|\.vaucanson|\.gitignore|\.gitmodules)$' | xargs echo)" HEAD

# Nettoyage du dépôt
git remote rm origin
git update-ref -d refs/original/refs/heads/master
git reflog expire --expire=now --all
git repack -ad

Compilation dans /lrde/dev

Compilation classique d'un paquet :

source /lrde/dev/profile && ./configure CXXFLAGS="-O3" CFLAGS="-O3" --prefix=/lrde/dev/$(uname -m)/stow/$(basename $PWD) && make && make install

Compilation de gcc :

Tests