diff options
Diffstat (limited to 'systems/knuth/local/lib/linew10.mf')
-rw-r--r-- | systems/knuth/local/lib/linew10.mf | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/systems/knuth/local/lib/linew10.mf b/systems/knuth/local/lib/linew10.mf new file mode 100644 index 0000000000..cab30e9801 --- /dev/null +++ b/systems/knuth/local/lib/linew10.mf @@ -0,0 +1,11 @@ +font_identifier "LINEW"; font_size 10pt#; +font_coding_scheme:="LATEX LINE"; +mode_setup; + +qqs#=.8pt#; %width of lines +qqh#=10pt#; %height of vertical stroke. +qqw#=10pt#; %length of horizontal stroke. + +%arrow dimensions: +arrowlen#=.6*qqw#; arrowht#=.22*qqw#; arrowcurve#=.1*arrowht#; +input line; |