The GitHub v.3 API for repository data returns an integer identifier for a given repository. This identifier is the value of the field id
in the data returned. In this example, it is the number 1296269:
[
{
"id": 1296269,
"owner": {
"login": "octocat",
... stuff omitted for brevity ...
},
"name": "Hello-World",
"full_name": "octocat/Hello-World",
... stuff omitted for brevity ...
}
]
Is a given identifier value ever reused once it is assigned to a repository, even if a repository or its owner account is subsequently deleted? In other words, are the identifiers unique and permanent, and never reused for any other repositories, ever?
In this context, I don't mean simply renaming a repository; that would not count as "reusing" it in the same sense, nor would replacing the content of a repository completely with other content. I am trying to understand specifically whether the GitHub id
values are ever "recycled", if you will.
(I honestly searched in the GitHub documentation and the web, but could not find a statement either way. If I missed it, I apologize and would be happy to be pointed to the appropriate documentation.)