diff options
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index 4791faf586..3f8c2a0518 100644 --- a/Makefile.common +++ b/Makefile.common @@ -73,7 +73,7 @@ SRCDIRS:=\ omega romega micromega quote ring dp \ setoid_ring xml extraction fourier \ cc funind firstorder field subtac \ - rtauto nsatz syntax decl_mode) + rtauto nsatz syntax decl_mode) # Order is relevent here because kernel and checker contain files # with the same name |