Hi all, I don't know if this has been raised before, but it seems not to be fixed yet. Currently, in HTML export, instead of #custom_id I'm getting e.g. #orgheadline10.
The commit that broke this was 2 months ago: 160820bc9498e9364103e72b55a27cf92576dbb8 still works fine. Let me know if this is bug that needs to be fixed, or maybe CUSTOM_ID was replaced with something. regards, Oleh
