Closed jerrymarino closed 4 years ago
For when we don't use a headermap, we use this instead. The current code added a few less directories than the original code.
Additionally, it cleans up the algorithms to use trivialize:
trivialize:
For when we don't use a headermap, we use this instead. The current code added a few less directories than the original code.
Additionally, it cleans up the algorithms to use
trivialize: