[O] Custom time stamps and HTML export and #+BIND

[Dominik, Carsten]

Hi Nicolas,

I have a file that I am exporting to HTML, and the file contains

#+BIND: org-time-stamp-custom-formats ("<%d-%m-%Y>" . "<%d-%m-%Y %H:%M>")
#+BIND: org-display-custom-times t

Apparently these lines are not used during HTML export.  I debugged the
org-translate-time function.  When it is called during HTML export, both
variables do not have the desired values.

This should still work, right?

- Carsten