diff options
| -rw-r--r-- | docs/index.css | 4 | ||||
| -rw-r--r-- | docs/index.html | 3 |
2 files changed, 6 insertions, 1 deletions
diff --git a/docs/index.css b/docs/index.css index 804f7749d..438eeebd0 100644 --- a/docs/index.css +++ b/docs/index.css @@ -70,6 +70,10 @@ dem { /* de-emphasize */ font-weight: 400; opacity: 0.7; } +num { /* number */ + font-feature-settings: 'calt' 1, 'ss01' 1; + white-space: pre; +} h1, h2, h3 { font-weight: 500; diff --git a/docs/index.html b/docs/index.html index b238bbd4a..764f68c9d 100644 --- a/docs/index.html +++ b/docs/index.html @@ -264,7 +264,8 @@ <li class="a"> Interface was developed in an a private, internal git repository starting in November 2016, prior to being published on August 22, 2017. - Between November 2016 and August 2017, there were 2 990 150 line edits made across 247 versions. + Between November 2016 and August 2017, there were + <num>2 990 150</num> line edits made across 247 versions. The reason the public GitHub repository does not reflect this is the fact that the project was initially only internal at the company where the author works and had some sensitive information "checked in", |