mirror of
https://github.com/jgm/pandoc.git
synced 2026-09-13 19:15:40 +00:00
This is needed for ghci to work with pandoc, given that we now use a custom prelude. Closes #2503.
This is needed for ghci to work with pandoc, given that we now use a custom prelude. Closes #2503.