use DejaVu font

build-notes.md

@@ -0,0 +1,9 @@
+# Build
+
+jupyter-book build contents
+jupyter-book build contents --builder pdfhtml
+git add ....
+git commit -m '....'
+git push github main
+cd contents
+ghp-import -r github -n -p -f _build/html

contents/_static/custom.css

@@ -1,8 +1,22 @@
+@font-face {
+ font-family: 'codefont';
+ src: local('DejaVu Sans Mono'),
+ local('APL385 Unicode'),
+ local('SImPL'),
+ url(https://aplwiki.com/images/7/75/DejaVuSansMono.ttf) format('truetype');
+}
+
+.CodeMirror pre {font-family: codefont, monospace;}
+
 /* Reduce excessive line height in code outputs */
 .output.text_html {
- font-family: 'APL385';
+ font-family: codefont, monospace;
  line-height: 0.95em;
 }
+/*.output.text_html {
+ font-family: 'APL385';
+ line-height: 0.95em;
+}*/
 
 /* Reduce excessive whitespace in tables */
 .table td, .table th {