Comment convertir du HTML en #

On peut recourir à l’application en ligne de commande pandoc. En supposant que le fichier HTML à convertir soit index.html, il suffit de lancer dans un terminal la commande :

pandoc  --standalone index.html --output index.tex

À faire

Cette réponse est à fusionner avec celle de la même question traitée ailleurs.