Compflags @since removal for .cmti files for odoc

master
John Whitington 2020-08-05 16:36:37 +01:00
parent 35cb3e550f
commit 5e5423b1f2
1 changed files with 1 additions and 0 deletions

View File

@ -32,6 +32,7 @@ case $1 in
stdlib__printf.cm[io]|stdlib__format.cm[io]|stdlib__scanf.cm[io])
echo ' -w Ae';;
stdlib__scanf.cmx) echo ' -inline 9';;
*Labels.cmi) echo ' -pp "$AWK -f ./expand_module_aliases.awk"';;
*Labels.cm[ox]) echo ' -nolabels -no-alias-deps';;
stdlib__float.cm[ox]) echo ' -nolabels -no-alias-deps';;
*) echo ' ';;