Add "view hidden" button to examples in HTML #619
Description
Use an eye icon. It should show ```imports blocks and ```lean -show``` blocks, but not lean -show -keep, as these latter are used exclusively for internal tests.
{{ message }}
Use an eye icon. It should show ```imports blocks and ```lean -show``` blocks, but not lean -show -keep, as these latter are used exclusively for internal tests.