[ #4457 ] A test case.

examples/Makefile

@@ -6,6 +6,7 @@ include $(TOP)/mk/paths.mk
 # Keep the `default` prerequisites in alphabetic order please!
 default : ac \
           aim4-bag \
+          compact-regions \
           divmod \
           effects \
           hello \
@@ -173,6 +174,12 @@ relocatable-interfaces : relocatable/originals/*.agda
 	@[ `grep "^ *Loading" relocatable/copies/output | wc -l` = 1 ]
 	@rm -rf relocatable/copies
 
+.PHONY : compact-regions
+compact-regions : relocatable/originals/*.agda
+	@$(echo) "Testing that --compact-regions works."
+	@$(agda) --ignore-interfaces --compact-regions -irelocatable/originals --no-libraries relocatable/originals/C.agda
+	@$(agda) --compact-regions -irelocatable/originals --no-libraries relocatable/originals/C.agda
+
 .PHONY : uptodate
 uptodate : uptodate/*.agda
 	@$(echo) "Testing that already imported modules are up-to-date" # despite having DOS line-endings