add name for git file

This commit is contained in:
Yann Dupont 2022-01-10 14:20:51 +01:00
parent 36fe52d91e
commit f3a98e94ed

View file

@ -296,6 +296,7 @@
(uri (git-reference
(url "https://oauth2:glpat-RsX2GjsD2WrzXubiJeou@gitlab.univ-nantes.fr/CCIPL/legacy_code_mirror/grace.git")
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256 (base32 "1wb8v0q8xa2akas0swpgdgw1s66i50k7kh1g2f894hnk91fzx56z"))
)
)