Contribuer

Il est possible de contribuer à ce resitory en y ajoutant des synthèses, des corrections d'APE ou simplement en modifiant celles déjà existantes.

Configurer git

Pour cela, il faut utiliser l' utilisation avancée et se créer un compte.

Editer

Faites maintenant les changements désirés.

Vous pouvez utiliser les Makefile de la manière suivante

$ make Pour compiler votre fichier .tex en .pdf.

$ make release Pour mettre votre fichier .pdf dans le dossier release au bon endroit.

Commiter et pusher

Ouvrez ensuite une console et déplacez vous dans le dossier Syntheses.

Ecrivez

$ git status

Vous pouvez alors voir les fichiers que vous avez modifié, ajouté et supprimé. Pour voir ce que vous avez modifié plus précisément sur fichier, écrivez

$ git diff -- fichier

Vous devez maintenant signaler les fichiers que vous avez modifié et que vous voulez commiter. Pour cela, il faut utiliser la commande add de git. Si vous voulez ajouter fichier, écrivez

$ git add fichier

Vous pouvez vérifier que ça a bien marché avec un $ git status. Quand vous êtes satisfait de ce que $git status dit qu'il va commiter, écrivez

$ git commit -m "Un message descriptif #12"

(Ici, je suppose que le commit résoud l'issue numéro 12 de github, c'est pas obligatoire mais ça permet à github d'afficher le commit dans la conversation de l'issue 12). Si vous oubliez le -m "foo", git va ouvrir votre éditeur de texte par défaut et attendre que vous écriviez la description du commit et que vous sauviez le fichier. Si vous le laissez vide, le commit sera annulé.

Vous pouvez maintenant apercevoir à l'aide d'un $ git log que vous avez fait un nouveau commit. Seulement, ce commit n'est pas encore sur github. Pour le mettre sur github, faites

$ git push origin master

Voilà, les autres développeurs peuvent maintenant bénéficier de vos commits à l'aide d'un $ git pull. Notez que si vous n'êtes pas enregistré en tant que contributeur, il faudra attendre qu'un contributeur accepte votre push en tant que valide avant de le voir sur github.

Si vous avez eu un problème. Regardez dans la FAQ si votre question a déjà été posée et résolue. Sinon, demandez ou cherchez sur Google.