Leo/oclaunch

mirror of https://gitlab.com/WzukW/oclaunch.git

Author	SHA1 Message	Date
Leo	3daa647382 Change indentation settings	9 years ago
Leo	2cfe7b5991 Fix indentation of fix-indent.ml script	9 years ago
Leo	22248b316e Fix issue of symlinks & ignored path in fix-indent.ml	9 years ago
Leo	c9bee871d3 Add script to fix indentation in the source code	9 years ago