 Bradley M. Kuhn
|
3a5872fab3
Properly format and place title everywhere.
|
10 年之前 |
|
Bradley M. Kuhn
|
fec40cd579
Make image a link back to the front page.
|
10 年之前 |
|
Bradley M. Kuhn
|
9563fd114a
Hopefully, <img> style same as svg had will work.
|
10 年之前 |
|
Bradley M. Kuhn
|
d2dcdb4c8a
Remove svg because users complain it's cut off.
|
10 年之前 |
|
Bradley M. Kuhn
|
983b035d68
Shorten these monikers for motion.
|
10 年之前 |
|
Bradley M. Kuhn
|
5f974f6655
See if I can get away with 50px here.
|
10 年之前 |
|
Bradley M. Kuhn
|
a3fc656222
Revert incorrect last commit.
|
10 年之前 |
|
Bradley M. Kuhn
|
8dd9077cce
Fix COnfigure (lower case O) and padding for svg
|
10 年之前 |
|
Bradley M. Kuhn
|
536550d424
Rework PDF/HTML selection to the top bar instead.
|
10 年之前 |
|
Bradley M. Kuhn
|
8100b728a6
HTML formatting fixes.
|
10 年之前 |
|
Bradley M. Kuhn
|
f9cc9a78f8
Attempts to get the tag matching right.
|
10 年之前 |
|
Bradley M. Kuhn
|
53a64ca4a1
Ensure that title appears properly.
|
10 年之前 |
|
Bradley M. Kuhn
|
816c59aa3d
Hack to get all menus to appear in right places.
|
10 年之前 |
|
Bradley M. Kuhn
|
988c791a78
These \IgnorePara and such can't be right.
|
10 年之前 |
|
Bradley M. Kuhn
|
38e093a8e2
Remove image, and add next/next+ config.
|
10 年之前 |
|
Bradley M. Kuhn
|
df3a2c0dc7
Better names for navigation operations.
|
10 年之前 |
|
Bradley M. Kuhn
|
9730276f9c
Don't necessarily move to right for navbar on top.
|
10 年之前 |
|
Bradley M. Kuhn
|
295f439fbd
configure crosslinks to work with bootstrap.
|
10 年之前 |
|
Bradley M. Kuhn
|
3f10dad1b9
fix closes on svg and img tags here.
|
10 年之前 |
|
Bradley M. Kuhn
|
681c5afd3f
Add \Hnewline on the end of all these lines.
|
10 年之前 |
|
Bradley M. Kuhn
|
e2f9cbe39a
Hacks to get top-bar branding on website.
|
10 年之前 |
|
Bradley M. Kuhn
|
4fc7088b9c
refer to favicon.ico
|
10 年之前 |
|
Bradley M. Kuhn
|
8512ac184a
Load bootstrap, assumed to be in /
|
10 年之前 |
|
Bradley M. Kuhn
|
913551b960
Add css for guide and include it from webhacks.
|
10 年之前 |
|
Bradley M. Kuhn
|
441df63ee7
Hack tex4ht's overlib stuff to use jQuery tooltip
|
10 年之前 |
