diff options
| -rwxr-xr-x | distrib/debian/rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/distrib/debian/rules b/distrib/debian/rules index f17072384b..e8e3aaea6b 100755 --- a/distrib/debian/rules +++ b/distrib/debian/rules @@ -21,7 +21,7 @@ build-stamp: dh_testdir # Add here commands to compile the package. - $(MAKE) -j world + $(MAKE) world #/usr/bin/docbook-to-man debian/coq.sgml > coq.1 touch build-stamp |