From 38355f0d95baf159926ca30f377cd86ed8636838 Mon Sep 17 00:00:00 2001
From: Samuel Thibault <samuel.thibault@ens-lyon.org>
Date: Tue, 9 Feb 2021 09:58:03 +0100
Subject: Note that one has to produce a 32bit mig

---
 microkernel/mach/mig/gnu_mig/building.mdwn | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'microkernel/mach/mig/gnu_mig')

diff --git a/microkernel/mach/mig/gnu_mig/building.mdwn b/microkernel/mach/mig/gnu_mig/building.mdwn
index 486c461e..2e155e75 100644
--- a/microkernel/mach/mig/gnu_mig/building.mdwn
+++ b/microkernel/mach/mig/gnu_mig/building.mdwn
@@ -48,6 +48,9 @@ Start the build process:
 
     $ dpkg-buildpackage -us -uc -b -rfakeroot
 
+Note: if you are building on a non-32bit system, you need to also pass e.g.
+`--target-arch=i386` to build the 32bit version.
+
 This will create a _.deb_ package in the parent directory,
 which you can then install on your system.
 
-- 
cgit v1.2.3