CI: wiki: add note about renamed devices (MR 3079)

Ask people to add renamed devices to https://postmarketos.org/renamed
The CI script already downloads this page and ignores missing devices
that are on this list of renamed devices. This is important, so when
creating a MR that renames a device, and already renaming the device in
the wiki, other CI jobs will not start failing until the MR is merged.
This commit is contained in:
Oliver Smith 2022-04-19 09:28:05 +02:00
parent ffeeba88a5
commit f940819e64
No known key found for this signature in database
GPG key ID: 5AE7F5513E0885CB

View file

@ -121,6 +121,10 @@ def main():
print("it more easily. Many times one person did a port with basic")
print("functionality, and then someone else jumped in and")
print("contributed major new features.")
print("")
print("NOTE: if you renamed a device in pmaports, rename it in the")
print("wiki as well and make sure to add it here:")
print("https://postmarketos.org/renamed")
return 1
else:
print("*** Wiki check successful!")