The value of $\sin(\pi/10)$