Show More
@@ -1,5 +1,9 b'' | |||
|
1 | 1 | # encoding: utf-8 |
|
2 | 2 | |
|
3 | # DO NOT EDIT THIS FILE BY HAND. | |
|
4 | ||
|
5 | # To update this file, run the script /tools/gen_latex_symbols.py using Python 3 | |
|
6 | ||
|
3 | 7 | # This file is autogenerated from the file: |
|
4 | 8 | # https://raw.githubusercontent.com/JuliaLang/julia/master/base/latex_symbols.jl |
|
5 | 9 | # This original list is filtered to remove any unicode characters that are not valid |
@@ -10,6 +10,11 b'' | |||
|
10 | 10 | # The original mapping of latex symbols to unicode comes from the `latex_symbols.jl` files from Julia. |
|
11 | 11 | |
|
12 | 12 | from __future__ import print_function |
|
13 | import os, sys | |
|
14 | ||
|
15 | if not sys.version_info[0] == 3: | |
|
16 | print("This script must be run with Python 3, exiting...") | |
|
17 | sys.exit(1) | |
|
13 | 18 | |
|
14 | 19 | # Import the Julia LaTeX symbols |
|
15 | 20 | print('Importing latex_symbols.js from Julia...') |
@@ -59,6 +64,10 b' valid_idents = [line for line in lines if test_ident(line[1])]' | |||
|
59 | 64 | |
|
60 | 65 | s = """# encoding: utf-8 |
|
61 | 66 | |
|
67 | # DO NOT EDIT THIS FILE BY HAND. | |
|
68 | ||
|
69 | # To update this file, run the script /tools/gen_latex_symbols.py using Python 3 | |
|
70 | ||
|
62 | 71 | # This file is autogenerated from the file: |
|
63 | 72 | # https://raw.githubusercontent.com/JuliaLang/julia/master/base/latex_symbols.jl |
|
64 | 73 | # This original list is filtered to remove any unicode characters that are not valid |
@@ -70,7 +79,9 b' for line in valid_idents:' | |||
|
70 | 79 | s += ' "%s" : "%s",\n' % (line[0], line[1]) |
|
71 | 80 | s += "}\n" |
|
72 | 81 | |
|
73 | with open('latex_symbols.py', 'w', encoding='utf-8') as f: | |
|
82 | fn = os.path.join('..','IPython','core','latex_symbols.py') | |
|
83 | print("Writing the file: %s" % fn) | |
|
84 | with open(fn, 'w', encoding='utf-8') as f: | |
|
74 | 85 | f.write(s) |
|
75 | 86 | |
|
76 | 87 |
General Comments 0
You need to be logged in to leave comments.
Login now