projects / git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bb72e10) | patch
CodingGuidelines: formatting HEAD in documentation
authorMatthieu Moy <Matthieu.Moy@imag.fr>
Tue, 28 Jun 2016 11:40:14 +0000 (13:40 +0200)
committerJunio C Hamano <gitster@pobox.com>
Tue, 28 Jun 2016 15:36:45 +0000 (08:36 -0700)
commit57103dbf702557abefc7c8c4578145f9383d6e9d
tree614e9428f4a7d859d7d2d4a6e652d6cbf60cfa2btree | snapshot
parentbb72e10a4196dda93afd8afba55e15fb1e5503c4commit | diff
CodingGuidelines: formatting HEAD in documentation

The current practice is:

git/Documentation$ git grep "'HEAD'" | wc -l
24
git/Documentation$ git grep "\`HEAD\`" | wc -l
66

Let's adopt the majority as a guideline.

Signed-off-by: Matthieu Moy <Matthieu.Moy@imag.fr>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Documentation/CodingGuidelines diff | blob | blame | history
Unnamed repository; edit this file 'description' to name the repository.