This allows us to override the value of the variable by simply defining
the --header-height CSS variable. The alternative is to add (or
subtract) a value to all places where $header-height is used if we want
to override it which is error prone and bloats our CSS files.