set.mm/scripts at develop · KyleWyonch/set.mm · GitHub

Name		Name	Last commit message	Last commit date
parent directory ..
README.md		README.md
build-metamath		build-metamath
calculate-all-dates		calculate-all-dates
calculate-dates		calculate-dates
captioner		captioner
check-braces		check-braces
check-dvs.py		check-dvs.py
check-raw-html		check-raw-html
count-all-steps		count-all-steps
count-steps		count-steps
count-usage		count-usage
date2unixts.py		date2unixts.py
download-avatars		download-avatars
download-metamath		download-metamath
find-repeats		find-repeats
gen-html		gen-html
gource-captions.txt		gource-captions.txt
gource.config		gource.config
gourcify		gourcify
iset-match.py		iset-match.py
jobs		jobs
jobs.makefile		jobs.makefile
latex_collector.py		latex_collector.py
linkify.py		linkify.py
list-theorems		list-theorems
mass-rename		mass-rename
min.cmd		min.cmd
minimize		minimize
minimize-all		minimize-all
missing-persons		missing-persons
mm100-achievable		mm100-achievable
mm100-mathboxed		mm100-mathboxed
regen-discouraged		regen-discouraged
regen-from-raw		regen-from-raw
rename-proposals		rename-proposals
report-changes.py		report-changes.py
rewrap		rewrap
typeset.py		typeset.py
unjunk.py		unjunk.py
verify		verify
verify-mmj2		verify-mmj2

README.md

This directory contains various scripts to work with metamath files.

Most are shell scripts (on Windows you can run them via Cygwin).

Most assume that the "metamath" executable is available.