Skip to content

Conversation

@TobiasWrigstad
Copy link
Collaborator

@TobiasWrigstad TobiasWrigstad commented Nov 14, 2021

This PR ignores sicpjs.ind and instead loads hand-paginated.ind for the final pagination.

@martin-henz
Copy link
Member

Looks promising :-)

@TobiasWrigstad
Copy link
Collaborator Author

@martin-henz I'm using my admin privileges to merge this now!

@TobiasWrigstad TobiasWrigstad merged commit 05d2f99 into master Nov 15, 2021
@martin-henz martin-henz changed the title WIP PR for hand-editing of index PR for hand-editing of index Nov 16, 2021
@RichDom2185 RichDom2185 deleted the index-hand-edits branch July 7, 2024 11:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

3 participants