Do not includie same directory multiple times

malc committed 5 years ago

Commit 19a2d361 parent 2d6bcb71 file · +4 −1Browse files

Unified · Split

build.bash+4−1

@@ -55,7 +55,10 @@ oincs() { · 54 unmodified lines
55	55	glutils.cmo) incs="-I $b -I $b/lablGL";;
56	56	uiutils.cmo\|main.cmo) incs="-I $b -I $b/$wsid -I $b/lablGL";;
57	57	ffi.cmo\|help.cmi\|parser.cmo) incs="-I $b";;
58		− config.cmo) incs="-I $b -I $b/$wsid -I $outd";;
	58	+ config.cmo)
	59	+ incs="-I $b -I $b/$wsid"
	60	+ test "$b" = $outd \|\| incs="$incs -I $outd"
	61	+ ;;
59	62	lablGL/*) incs="-I $b/lablGL";;
60	63	main.cmi\|keys.cmo\|utils.cmo\|utf8syms.cmo) ;;
61	64	*) die "ocaml include paths for '$2' aren't set";;