A few hashes have special characters in them. Namely hashes of builtin terms, for instance divide: ##Nat./.
When rendering this to the URL or using it as in an API request, we want to URI encode everything but the # symbols, which should be replaced with @. Note that there can be multiple # symbols in the string at multiple locations.
hojberg
commented
2 years ago
A few hashes have special characters in them. Namely hashes of builtin terms, for instance divide:
##Nat./.When rendering this to the URL or using it as in an API request, we want to URI encode everything but the
#symbols, which should be replaced with@. Note that there can be multiple#symbols in the string at multiple locations.