J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir

noté cette erreur de ma part (copier/coller mon amour).

Ça créait des soucis dans les dépendance dans l'ancienne architecture de 
Makefile, probablement dans la nouvelle aussi dans certaines 
circonstances. Exit les bêtise, c'est plus propre maintenant.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10019 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions