Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Turn the "eternal" handbook date into symbols #1021

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Turn the "eternal" handbook date into symbols #1021

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions docs/conf.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,9 @@
autorunrecord_line_replace = [
# trailing space removal
(r'[ ]+$', ''),
# turn our "eternal" date time into symbols
(r'Tue Jun 18 16:13:00 2019 +0000', '🗓🕓'),
(r'2019-06-18 16:13', '🗓🕓'),
Comment on lines +38 to +39
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see two reasons why the regexp would not work:

  • The plus symbol needs to be escaped (otherwise it's "space, one or more, followed by 0000")
  • The time zone can not be taken for granted, the config sets git author & committer date to 2019-06-18T16:13:00, and for me this produces run records with git log saying Tue Jun 18 16:13:00 2019 +0200 (I'm in CEST).

I'm also adding a space for IMHO better aesthetics.

Suggested change
(r'Tue Jun 18 16:13:00 2019 +0000', '🗓🕓'),
(r'2019-06-18 16:13', '🗓🕓'),
(r'Tue Jun 18 16:13:00 2019 \+\d{4}', '🗓 🕓'),
(r'2019-06-18 16:13', '🗓 🕓'),

Comment on lines +38 to +39
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As a side note, I would use 📅 (Calendar, U+1F4C5) instead of 🗓 (Spiral Calendar Pad, U+1F5D3), but that's a personal preference and likely depends on my set of browser fonts (?) -- not leaving a GitHub suggestion as this would require a one-line change to fontpkg.sty, too.

# strip the keydir for MD5(E) or SHA1(E) annex keys
# the keydir is identical to the annex key name, but consumes
# a lot of space. we replace it with a UTF scissors icon
Expand Down
6 changes: 4 additions & 2 deletions docs/latex/fontpkg.sty
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@
\usepackage{microtype}

% provide definition for Unicode character ✂ (U+2702) we use for truncation
\usepackage{marvosym}
\usepackage{fontawesome}
\usepackage{newunicodechar}
\newunicodechar{✂}{\Rightscissors}
\newunicodechar{✂}{\faScissors}
\newunicodechar{🗓}{\faCalendar}
\newunicodechar{🕓}{\faClockO}