diff --git a/docs/MAKE b/docs/MAKE new file mode 100644 index 0000000..d5d1faa --- /dev/null +++ b/docs/MAKE @@ -0,0 +1,7 @@ +python build_index.py ./source/index.md > ./html/index.html +python build_index.py ./source/Thun.md > html/Thun.html +python build_index.py ./source/notebooks/BigNums.md > ./html/notebooks/BigInts.html +python build_index.py ./source/notebooks/Generator_Programs.md > ./html/notebooks/Generator_Programs.html +(cd ../implementations/Elm/ ; make) +cp -f ../implementations/Elm/demo/Joy.js ./html/Joy.js + diff --git a/docs/build_index.py b/docs/build_index.py index d66cafc..894c569 100644 --- a/docs/build_index.py +++ b/docs/build_index.py @@ -21,9 +21,12 @@ print(f'''\