Use repo ID rather than path in header (fixes #425)

This commit is contained in:
Jakob Borg
2014-08-03 21:58:36 +02:00
parent 327cd4cb87
commit 6f724a113c
2 changed files with 2 additions and 2 deletions

File diff suppressed because one or more lines are too long