Indentation issue on online code blocks

[yblein]

There is an issue with the indentation in the code blocks of the online tutorial: tabs and spaces appear to be mixed up. The following example illustrates this on the lines inside the calc environment:

theorem zero_add (n : nat) : 0 + n = n :=
induction_on n
  (show 0 + 0 = 0, from rfl)
  (take n,
    assume IH : 0 + n = n,
    show 0 + succ n = succ n, from
      calc
    0 + succ n = succ (0 + n) : rfl
      ... = succ n : IH)

Of course it looks fine on Github which is using 8 spaces for tabs, but it does not on the online tutorial which is using 4 spaces in code blocks. This makes code blocks a little wonky. Since the original source code is fine (all spaces), I guess some tool is trying to be smarter than it should during the conversion and swaps 8 spaces sequences for a tab.

[gebner]

Thanks for pointing this out!

The issue was not at all related to github using 8 spaces for tabs. In fact, the *.org files all use spaces and no tabs at all! As you guessed, the problem was that the emacs org-mode export silently changed spaces to tabs, here is a related stackexchange post: http://emacs.stackexchange.com/questions/24283/org-mode-converting-spaces-to-tabs-when-evaluating-source